X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=dfc61de151fa83e058f234f30fdc0f2438d0dd1b;hb=ede00573e3e4cb28df7ca9a5dae6228c2b432608;hp=9135ff24d72787e8835f9d1cb7b75898f4c4f2d0;hpb=397413c4196f84c81d61ba7dd79b54ab1c428ebb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 9135ff24d..dfc61de15 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/constructors/uparrow_1.ma".
+include "ground_2/notation/functions/uparrow_1.ma".
 include "ground_2/notation/functions/downarrow_1.ma".
 include "arithmetics/nat.ma".
 include "ground_2/lib/relations.ma".
@@ -57,17 +57,27 @@ lemma plus_SO: ∀n. n + 1 = ↑n.
 lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
 // qed-.
 
+lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
+// qed.
+
+lemma arith_l (n1) (n2): ↑n2-n1 = 1-n1+(n2-(n1-1)).
+* // qed.
+
+lemma arith_l_eq: ∀x. 1 = 1-x+(x-(x-1)).
+// qed.
+
 (* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
 lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
 #x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
 qed-.
 
+lemma lt_succ_pred: ∀m,n. n < m → m = ↑↓m.
+#m #n #Hm >S_pred /2 width=2 by ltn_to_ltO/
+qed-.
+
 fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y.
 /2 width=1 by plus_minus_minus_be/ qed-.
 
-lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
-// qed.
-
 lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p).
 /2 by plus_minus/ qed-.
 
@@ -139,6 +149,9 @@ fact le_repl_sn_trans_aux: ∀x,y,z:nat. x ≤ z → y = x → y ≤ z.
 lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
 /3 width=1 by monotonic_le_minus_l/ qed.
 
+lemma minus_le_trans_sn: ∀x1,x2. x1 ≤ x2 → ∀x. x1-x ≤ x2.
+/2 width=3 by transitive_le/ qed.
+
 (* Note: this might interfere with nat.ma *)
 lemma monotonic_lt_pred: ∀m,n. m < n → 0 < m → pred m < pred n.
 #m #n #Hmn #Hm whd >(S_pred … Hm)
@@ -255,6 +268,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-.