+theorem nle_zero_1: \forall q. zero <= q.
+ intros. auto.
+qed.
+
+theorem nle_succ_succ: \forall p,q. p <= q \to succ p <= succ q.
+ intros. elim H. clear H. auto.
+qed.
+
+theorem nle_ind: \forall P:(Nat \to Nat \to Prop).
+ (\forall n:Nat.P zero n) \to
+ (\forall n,n1:Nat.
+ n <= n1 \to P n n1 \to P (succ n) (succ n1)
+ ) \to
+ \forall n,n1:Nat. n <= n1 \to P n n1.
+ intros 4. elim n; clear n;
+ [ auto
+ | lapply linear nle_inv_succ_1 to H3. decompose; subst.
+ auto
+ ].
+qed.
+