- 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
- ].
-qed.
-
-theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y.
- intros. elim H using nle_ind; clear H x y;
- [ elim n; clear n; auto
- | decompose; subst; auto
- ].