milestone update in ground, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_plus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index f7d79ccdf3914095f44acde0d5689a4c48d6082c..40beec972819238df4a5bdd75ed92e403d48d436 100644 (file)
--- 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,10 +42,12 @@ 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) ****************************)
@@ -63,7 +65,7 @@ qed.
 (*** commutative_plus *)
 lemma nplus_comm: commutative … nplus.
 #m @(nat_ind_succ … m) -m //
-qed-.
+qed-. (**) (* gets in the way with auto *)
 
 (*** associative_plus *)
 lemma nplus_assoc: associative … nplus.
@@ -91,11 +93,12 @@ qed-.
 
 (* Basic inversions *********************************************************)
 
-lemma eq_inv_nzero_plus (m) (n): 𝟎 = m + n → ∧∧ 𝟎 = m & 𝟎 = n.
+(*** plus_inv_O3 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/
 | #n #_ <nplus_succ_dx #H
-  elim (eq_inv_nzero_succ … H)
+  elim (eq_inv_zero_nsucc … H)
 ]
 qed-.
 
@@ -110,6 +113,27 @@ lemma eq_inv_nplus_bi_sn (o) (m) (n): o + m = o + n → m = n.
 /2 width=2 by eq_inv_nplus_bi_dx/
 qed-.
 
+(*** plus_xSy_x_false *)
+lemma succ_nplus_refl_sn (m) (n): m = ↑(m + n) → ⊥.
+#m @(nat_ind_succ … m) -m
+[ /2 width=2 by eq_inv_zero_nsucc/
+| #m #IH #n #H
+  @(IH n) /2 width=1 by eq_inv_nsucc_bi/
+]
+qed-.
+
+(*** discr_plus_xy_y *)
+lemma nplus_refl_dx (m) (n): n = m + n → 𝟎 = m.
+#m #n @(nat_ind_succ … n) -n //
+#n #IH /3 width=1 by eq_inv_nsucc_bi/
+qed-.
+
+(*** discr_plus_x_xy *)
+lemma nplus_refl_sn (m) (n): m = m + n → 𝟎 = n.
+#m #n <nplus_comm
+/2 width=2 by nplus_refl_dx/
+qed-.
+
 (* Advanced eliminations ****************************************************)
 
 (*** nat_ind_plus *)