-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.
-
-theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y.
- intros. elim H using nle_ind; clear H x y; auto.
-qed.
-
-theorem nle_false: \forall x,y. x <= y \to y < x \to False.
- intros 3; elim H using nle_ind; clear H x y; auto.
-qed.
-
-theorem nle_trans: \forall x,y. x <= y \to
- \forall z. y <= z \to x <= z.
- intros 3. elim H using nle_ind; clear H x y;
- [ auto
- | lapply linear nle_inv_succ_1 to H3. decompose. subst.
- auto
- ].
+theorem nle_trans_succ: ∀x,y. x ≤ y → x ≤ succ y.
+ intros; elim H; clear H x y; autobatch.