propagating the arithmetics library, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / mr2_plus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/mr2_plus.ma b/matita/matita/contribs/lambdadelta/ground/relocation/mr2_plus.ma
index 07374a027d845560ef722c68452522cef322e845..29c76eb3369b2ce8d83c17745dfa1a8b338982df 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/mr2_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/mr2_plus.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/arith/nat_minus_plus.ma".
 include "ground/relocation/mr2.ma".
 
 (* MULTIPLE RELOCATION WITH PAIRS *******************************************)
@@ -26,7 +27,7 @@ interpretation "plus (multiple relocation with pairs)"
 
 (* Basic properties *********************************************************)
 
-lemma pluss_SO2: ∀l,m,cs. (❨l,m❩;cs) + 1 = ❨↑l,m❩;cs + 1.
+lemma pluss_SO2: ∀l,m,cs. ((❨l,m❩;cs) + 𝟏) = ❨↑l,m❩;cs + 𝟏.
 normalize // qed.
 
 (* Basic inversion lemmas ***************************************************)
@@ -41,6 +42,6 @@ lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = ❨l,m❩;cs2 →
 #i #l #m #cs2 *
 [ normalize #H destruct
 | #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct
-  <minus_plus_m_m /2 width=3 by ex2_intro/
+  <nminus_plus_sn_refl_sn /2 width=3 by ex2_intro/
 ]
 qed-.