-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.
-
-theorem nle_refl: \forall x. x <= x.
- intros 1; elim x; clear x; intros; auto.
-qed.