Hola Bruno.
Has avanzado mucho, felicitaciones!
Pueden usar tácticas adicionales, mientras entiendan bien que están haciendo, no hoy problema. De a poco en el curso esto se irá viendo y se permitirá usar algunas cosas de Coq incluso adicionales a las que veamos en el curso.
Saludos Carlos