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

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