X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fpnat_plus.ma;h=af5bd09432c8b3460d1d5123d9c0f3ecd56bb819;hb=775ab35f714568dfcd672f0dd53a00e1ba7382cd;hp=c5c6ade72cc63a23b7e66a659590000f3cc2e327;hpb=21de0d35017656c5a55528390b54b0b2ae395b44;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index c5c6ade72..af5bd0943 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -17,7 +17,7 @@ include "ground/arith/pnat_iter.ma".
 (* ADDITION FOR POSITIVE INTEGERS *******************************************)
 
 definition pplus: pnat → pnat → pnat ≝
-           λp,q. psucc^q p.
+           λp,q. (psucc^q) p.
 
 interpretation
   "plus (positive integers)"
@@ -25,7 +25,7 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma pplus_one_dx (p): ↑p = p + 𝟏.
+lemma pplus_unit_dx (p): ↑p = p + 𝟏.
 // qed.
 
 lemma pplus_succ_dx (p) (q): ↑(p+q) = p + ↑q.
@@ -37,15 +37,37 @@ lemma pplus_succ_sn (p) (q): ↑(p+q) = ↑p + q.
 #p #q @(piter_appl … psucc)
 qed.
 
-lemma pplus_one_sn (p): ↑p = 𝟏 + p.
+lemma pplus_unit_sn (p): ↑p = 𝟏 + p.
 #p elim p -p //
 qed.
 
 lemma pplus_comm: commutative … pplus.
 #p elim p -p //
-qed-.
+qed-. (* * gets in the way with auto *)
 
 lemma pplus_assoc: associative … pplus.
 #p #q #r elim r -r //
 #r #IH <pplus_succ_dx <pplus_succ_dx <IH -IH //
 qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_unit_pplus (p) (q): 𝟏 = p + q → ⊥.
+#p #q elim q -q
+[ <pplus_unit_dx #H destruct
+| #q #_ <pplus_succ_dx #H destruct
+]
+qed-.
+
+lemma eq_inv_pplus_unit (p) (q):
+      p + q = 𝟏 → ⊥.
+/2 width=3 by eq_inv_unit_pplus/ qed-.
+
+lemma eq_inv_pplus_bi_dx (r) (p) (q): p + r = q + r → p = q.
+#r elim r -r /3 width=1 by eq_inv_psucc_bi/
+qed-.
+
+lemma eq_inv_pplus_bi_sn (r) (p) (q): r + p = r + q → p = q.
+#r #p #q <pplus_comm <pplus_comm in ⊢ (???%→?);
+/2 width=2 by eq_inv_pplus_bi_dx/
+qed-.