Unified-Sub: lift_comm completed

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

diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma b/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma
index e42eecde3ab305988f00002ac8f8cf12b83ec1a0..67a18d820de92b2201c5abe9403d7a7181678b7b 100644 (file)
--- a/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma
@@ -18,9 +18,9 @@ include "NPlus/inv.ma".
 include "NLE/defs.ma".
 
 theorem nle_inv_succ_1: \forall x,y. x < y \to 
-                         \exists z. y = succ z \land x <= z.
+                        \exists z. y = succ z \land x <= z.
  intros. elim H.
- lapply linear nplus_gen_succ_2 to H1.
+ lapply linear nplus_inv_succ_2 to H1.
  decompose. subst. auto depth = 4.
 qed.