Hola Eliana
Lo que hicieron está muy bien y queda una solución modular y comprensible.
Se puede trabajar con enteros en Coq, pero no se pedía (sobre enteros, si querés, podés ver por ejemplo: https://coq.inria.fr/library/Coq.ZArith.Int.html).
Saludos, Carlos