(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/RELATIONAL/NLE/props".
+
include "NLE/order.ma".
-theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y.
- intros. elim H; clear H x y; autobatch.
+theorem nle_trans_succ: ∀x,y. x ≤ y → x ≤ succ y.
+ intros; elim H; clear H x y; autobatch.
qed.
-theorem nle_gt_or_le: \forall x, y. y > x \lor y <= x.
+theorem nle_gt_or_le: ∀x, y. y > x ∨ y ≤ x.
intros 2; elim y; clear y;
[ autobatch
| decompose;
[ lapply linear nle_inv_succ_1 to H1
| lapply linear nle_lt_or_eq to H1
- ]; decompose; subst; autobatch depth = 4
+ ]; decompose; destruct; autobatch depth = 4
].
qed.