Hola.
Los casos podés generarlos usando por ejemplo elim (le_gt_dec (b-1) nn), donde nn saldrá luego de eliminar la hipótesis inductiva.
Mirando arriba podés hacer destruct x.
Saludos, Carlos
Hola.
Los casos podés generarlos usando por ejemplo elim (le_gt_dec (b-1) nn), donde nn saldrá luego de eliminar la hipótesis inductiva.
Mirando arriba podés hacer destruct x.
Saludos, Carlos