Se me complico el predicado Gt...intento:
Gt_n : Gt (S n) n
y me dice que
Error:
Last occurrence of "Gt" must have "n" as 1st argument in
"Gt (S n) n".
Se me ocurre definir Gt como negando Le (~Le)...pero no sé si esa es la idea??
También tengo definida la función Lebool pero no sé como utilizarla.