Hola!
Cuando mando al archivo ejecutar desde el inicio hasta el final con el botón de "Go to end", corre todas las líneas rápido excepto en la parte 5.3 en la línea que dice "Require Import Omega.", donde demora unos segundos y luego sigue rápido (todo compila correctamente).
¿Esto puede ser por algún problema o es normal? ¿será porque no hago la importación al inicio de la Section sino en el medio? ¿a alguien más le pasó?
Gracias.
Saludos!