X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fmr2_at.ma;h=6d60ead1bd4cdeb1fddec63a3e0aa2491a7d9fed;hp=51ac826b08e633f66d17cb6a344f5d04b92f7ea1;hb=8fdf1af656038d0245eba64ff2531bbe94ce0e9e;hpb=77c9255de3c5f7780aeacd745703a1cc76328a68

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/mr2_at.ma b/matita/matita/contribs/lambdadelta/ground/relocation/mr2_at.ma
index 51ac826b0..6d60ead1b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/mr2_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/mr2_at.ma
@@ -13,6 +13,8 @@
 (**************************************************************************)
 
 include "ground/notation/relations/rat_3.ma".
+include "ground/arith/nat_plus.ma".
+include "ground/arith/nat_lt.ma".
 include "ground/relocation/mr2.ma".
 
 (* MULTIPLE RELOCATION WITH PAIRS *******************************************)
@@ -61,14 +63,14 @@ lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @❪i1, ❨l, m❩;cs❫ ≘ i2 →
                       i1 < l → @❪i1, cs❫ ≘ i2.
 #cs #l #m #i1 #m2 #H
 elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l
-elim (lt_le_false … Hi1l Hli1)
+elim (nlt_ge_false … Hi1l Hli1)
 qed-.
 
 lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @❪i1, ❨l, m❩;cs❫ ≘ i2 →
                       l ≤ i1 → @❪i1 + m, cs❫ ≘ i2.
 #cs #l #m #i1 #m2 #H
 elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1
-elim (lt_le_false … Hi1l Hli1)
+elim (nlt_ge_false … Hi1l Hli1)
 qed-.
 
 (* Main properties **********************************************************)