Como la definición de nat junto a sus axiomas está hecha en la sección Ejercicio10, puede ser que al escribir End Ejercicio10. estemos perdiendo estas definiciones?
Al menos no me deja usarlas si no comento la línea End Ejercicio10..
Asumo que era la idea usarlos.
Saludos!