refactoring

[helm.git] / helm / software / matita / contribs / RELATIONAL / NLE / props.ma

diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma
index 34e5d0a242c42b541ef257f1f6a450721f712887..eccc2f9db3f69974cedaeda2b1ec387601bf394b 100644 (file)
--- a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/RELATIONAL/NLE/props".
 
-include "NLE/fwd.ma".
+include "NLE/inv.ma".
 
 theorem nle_zero_1: \forall q. zero <= q.
  intros. auto.
@@ -64,3 +64,15 @@ theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y.
  | decompose; subst; auto
  ].
 qed.
+
+theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x.
+ intros 2; elim y; clear y;
+ [ auto
+ | decompose;
+   [ lapply linear nle_inv_succ_1 to H1. decompose.
+     subst. auto depth=4
+   | lapply linear nle_lt_or_eq to H1; decompose;
+     subst; auto
+   ]
+ ].
+qed.