X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_plus.ma;h=75349d2da6281f130d0e2a0b3ea8930e379267f0;hb=5e72e41f4f86814e56d4b00959ccc56c71042a4c;hp=ffb181cc4908dea0a5048498cb6c2a11a453f56a;hpb=df7a2aa19e98dc28e7f22129275a175cead49e2d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index ffb181cc4..75349d2da 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/arith/nat_iter_succ.ma".
+include "ground/arith/nat_succ_iter.ma".
 
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* ADDITION FOR NON-NEGATIVE INTEGERS ***************************************)
 
 (*** plus *)
 definition nplus: nat → nat → nat ≝
@@ -33,7 +33,7 @@ lemma nplus_zero_dx (m): m = m + 𝟎.
 lemma nplus_one_dx (n): ↑n = n + 𝟏.
 // qed.
 
-(* Semigroup properties *****************************************************)
+(* Advanved rewrites (semigroup properties) *********************************)
 
 (*** plus_n_Sm *)
 lemma nplus_succ_dx (m) (n): ↑(m+n) = m + ↑n.
@@ -54,15 +54,20 @@ lemma nplus_comm: commutative … nplus.
 #m @(nat_ind … m) -m //
 qed-.
 
-lemma nplus_one_sn (n): ↑n = 𝟏 + n.
-#n <nplus_comm // qed.
-
 (*** associative_plus *)
 lemma nplus_assoc: associative … nplus.
 #m #n #o @(nat_ind … o) -o //
 #o #IH <nplus_succ_dx <nplus_succ_dx <nplus_succ_dx <IH -IH //
 qed.
 
+(* Advanced constructions ***************************************************)
+
+lemma nplus_one_sn (n): ↑n = 𝟏 + n.
+#n <nplus_comm // qed.
+
+lemma nplus_succ_shift (m) (n): ↑m + n = m + ↑n.
+// qed-.
+
 (*** assoc_plus1 *)
 lemma nplus_plus_comm_12 (o) (m) (n): m + n + o = n + (m + o).
 #o #m #n <nplus_comm in ⊢ (??(?%?)?); // qed.
@@ -88,7 +93,8 @@ qed-.
 (*** injective_plus_r *)
 lemma eq_inv_nplus_bi_sn (o) (m) (n): o + m = o + n → m = n.
 #o #m #n <nplus_comm <nplus_comm in ⊢ (???%→?);
-/2 width=2 by eq_inv_nplus_bi_dx/ qed-.
+/2 width=2 by eq_inv_nplus_bi_dx/
+qed-.
 
 (* Advanced eliminations ****************************************************)