Hola.
No me queda claro cual es el objetivo de este ejercicio.
La idea es definir una función que implemente el algoritmo dado y usarla de witness para demostrar nat_div_mod?
O el objetivo es demostrar nat_div_mod a fuerza de tácticas, siguiendo la lógica del algoritmo y luego extraer?
Saludos.
Hola.
La segunda opción es la indicada.
Saludos, Carlos
Hola, ¿La idea para resolver este ejercicio es definir la función divmod como un Function divmod y luego hacer un exists con eso?
¿Donde puedo leer bien qué hacen los módulos que hay que importar?
Saludos,
Jairo.
Hola Jairo.
En otro mail ya se comentó esto. La idea es seguir la lógica de la función utilizando tácticas.
El contenido de las librerías/bibliotecas puede consultarse en:
https://coq.inria.fr/distrib/current/stdlib/.
Saludos, Carlos
