X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_plus.ma;h=75ff371fb108a84e9847927ca670fd2af4c822f5;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hp=2df064a0189c3085ed0707a78532215d5e6bd79c;hpb=19b0a814861157ba05f23877d5cd94059f52c2e8;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 2df064a01..75ff371fb 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
@@ -21,7 +21,7 @@ definition nplus: nat → nat → nat ≝
            λm,n. nsucc^n m.
 
 interpretation
-  "plus (positive integers)"
+  "plus (non-negative integers)"
   'plus m n = (nplus m n).
 
 (* Basic constructions ******************************************************)
@@ -42,13 +42,15 @@ qed.
 (* Constructions with niter *************************************************)
 
 (*** iter_plus *)
-lemma niter_plus (A) (f) (a) (n1) (n2):
-      f^n1 (f^n2 a) = f^{A}(n1+n2) a.
-#A #f #a #n1 #n2 @(nat_ind_succ … n2) -n2 //
-#n2 #IH <nplus_succ_dx <niter_succ <niter_succ <niter_appl //
+lemma niter_plus (A) (f) (n1) (n2):
+      f^n2 ∘ f^n1 ≐ f^{A}(n1+n2).
+#A #f #n1 #n2 @(nat_ind_succ … n2) -n2 //
+#n2 #IH <nplus_succ_dx
+@exteq_repl
+/3 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
 qed.
 
-(* Advanved constructions (semigroup properties) ****************************)
+(* Advanced constructions (semigroup properties) ****************************)
 
 (*** plus_S1 *)
 lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.
@@ -63,7 +65,7 @@ qed.
 (*** commutative_plus *)
 lemma nplus_comm: commutative … nplus.
 #m @(nat_ind_succ … m) -m //
-qed-. (**) (* gets in the way with auto *)
+qed-. (* * gets in the way with auto *)
 
 (*** associative_plus *)
 lemma nplus_assoc: associative … nplus.
@@ -78,7 +80,7 @@ lemma nplus_one_sn (n): ↑n = 𝟏 + n.
 #n <nplus_comm // qed.
 
 lemma nplus_succ_shift (m) (n): ↑m + n = m + ↑n.
-// qed-.
+// qed.
 
 (*** assoc_plus1 *)
 lemma nplus_plus_comm_12 (o) (m) (n): m + n + o = n + (m + o).
@@ -87,11 +89,11 @@ lemma nplus_plus_comm_12 (o) (m) (n): m + n + o = n + (m + o).
 (*** plus_plus_comm_23 *)
 lemma nplus_plus_comm_23 (o) (m) (n): o + m + n = o + n + m.
 #o #m #n >nplus_assoc >nplus_assoc <nplus_comm in ⊢ (??(??%)?); //
-qed-.
+qed.
 
 (* Basic inversions *********************************************************)
 
-(*** plus_inv_O3 zero_eq_plus *) 
+(*** zero_eq_plus *)
 lemma eq_inv_zero_nplus (m) (n): 𝟎 = m + n → ∧∧ 𝟎 = m & 𝟎 = n.
 #m #n @(nat_ind_succ … n) -n
 [ /2 width=1 by conj/
@@ -100,6 +102,11 @@ lemma eq_inv_zero_nplus (m) (n): 𝟎 = m + n → ∧∧ 𝟎 = m & 𝟎 = n.
 ]
 qed-.
 
+(*** plus_inv_O3 *)
+lemma eq_inv_nplus_zero (m) (n):
+      m + n = 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n.
+/2 width=1 by eq_inv_zero_nplus/ qed-.
+
 (*** injective_plus_l *)
 lemma eq_inv_nplus_bi_dx (o) (m) (n): m + o = n + o → m = n.
 #o @(nat_ind_succ … o) -o /3 width=1 by eq_inv_nsucc_bi/