update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / lib / arith.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 6f018ea257b32e20678e0793f33bb36c3a7560ab..1c13de648461fd98930fda4c197b28cab400c2fb 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -259,6 +259,22 @@ qed-.
 lemma plus_inv_O3: ∀x,y. x + y = 0 → x = 0 ∧ y = 0.
 /2 width=1 by plus_le_0/ qed-.
 
+lemma plus_inv_S3_sn: ∀x1,x2,x3. x1+x2 = ↑x3 →
+                      ∨∨ ∧∧ x1 = 0 & x2 = ↑x3
+                       | ∃∃y1. x1 = ↑y1 & y1 + x2 = x3.
+* /3 width=1 by or_introl, conj/
+#x1 #x2 #x3 <plus_S1 #H destruct
+/3 width=3 by ex2_intro, or_intror/
+qed-.
+
+lemma plus_inv_S3_dx: ∀x2,x1,x3. x1+x2 = ↑x3 →
+                      ∨∨ ∧∧ x2 = 0 & x1 = ↑x3
+                       | ∃∃y2. x2 = ↑y2 & x1 + y2 = x3.
+* /3 width=1 by or_introl, conj/
+#x2 #x1 #x3 <plus_n_Sm #H destruct
+/3 width=3 by ex2_intro, or_intror/
+qed-.
+
 lemma max_inv_O3: ∀x,y. (x ∨ y) = 0 → 0 = x ∧ 0 = y.
 /4 width=2 by le_maxr, le_maxl, le_n_O_to_eq, conj/
 qed-.