Print le.
Hint Resolve le_n le_S.

Lemma cero:forall n, 0<=n.
induction n;auto.
Qed.

Hint Resolve cero.

Lemma ccero:forall n m, n<=m -> (S n) <= (S m).

induction 1;auto.
Qed.
Hint Resolve ccero.

Lemma uno:forall n,~(le (S n) 0).
intros n H.
inversion H.
Qed.
Hint Resolve uno.

Inductive me:nat->nat->Prop :=
me_0:forall n,me 0 n
|me_S:forall n m,me n m -> me (S n) (S m).
Hint Resolve me_0 me_S.

Lemma dos:forall n, me n n.
induction n;auto.
Qed.
Hint Resolve dos.

Lemma tres:forall n m, me n m -> me n (S m).
induction 1;auto.
Qed.
Hint Resolve tres.

Lemma equiv1:forall n m, n <= m -> me n m.
induction 1;auto.
Qed.

Lemma equiv2:forall n m, me n m -> n <= m.
induction 1;auto.
Qed.

 Print ex.

Require Export ZArithRing.

Theorem existe:forall n m, n<=m -> (exists p,n+p=m).
induction 1.
exists 0;auto.
case IHle.
intros.
rewrite <- H0.
exists (S x). 
ring_nat.
Qed.