Hola,
Estoy trancado en este ejercicio, lo que hice hasta ahora es como se indica en la sugerencia, hacer induccion en a; el caso a=0 sale sin problemas, para el caso inductivo no estoy viendo como dividir en casos (b-1 <= r o b-1 > r) ;
Al eliminar la hipotesis inductiva, obtengo:
x : nat * nat
p : let (q, r) := x in a = b * q + r /\ r < b
Pero no se como usar p.
Alguna sugerencia?
Saludos.