Hola.
El predicado Gt lo podés definir inductivamente. Por ejemplo:
Inductive Gt : nat -> nat -> Prop :=
| GtO : forall n : nat, Gt (S n) 0
| GtS : forall n m : nat, Gt n m -> Gt (S n) (S m).
Saludos, Carlos
Hola.
El predicado Gt lo podés definir inductivamente. Por ejemplo:
Inductive Gt : nat -> nat -> Prop :=
| GtO : forall n : nat, Gt (S n) 0
| GtS : forall n m : nat, Gt n m -> Gt (S n) (S m).
Saludos, Carlos