X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FRELATIONAL%2FNLE%2Finv.ma;h=67a18d820de92b2201c5abe9403d7a7181678b7b;hb=b0b69bb764af48d7f022477398f0beff5fb3f3f3;hp=e42eecde3ab305988f00002ac8f8cf12b83ec1a0;hpb=00f8f919262e3c84dd9e42477092cc1312171493;p=helm.git

diff --git a/matita/contribs/RELATIONAL/NLE/inv.ma b/matita/contribs/RELATIONAL/NLE/inv.ma
index e42eecde3..67a18d820 100644
--- a/matita/contribs/RELATIONAL/NLE/inv.ma
+++ b/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.