(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/RELATIONAL/NLE/props".
+
include "NLE/order.ma".
| 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.