update in binaries for λδ

[helm.git] / matita / matita / lib / arithmetics / nat.ma

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 249bd274e74622e59d69ab7d77782a86c713bc4d..cca4782806c2264ce0bc294a84bee55881d4a18c 100644 (file)
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -475,6 +475,11 @@ lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
 #m #n elim (decidable_le m n) /2/ /4/
 qed-.
 
+lemma le_inv_S1: ∀x,y. S x ≤ y → ∃∃z. x ≤ z & y = S z.
+#x #y #H elim H -y /2 width=3 by ex2_intro/
+#y #_ * #n #Hxn #H destruct /3 width=3 by le_S, ex2_intro/
+qed-. 
+
 (* More general conclusion **************************************************)
 
 theorem nat_ind_plus: ∀R:predicate nat.
@@ -531,6 +536,19 @@ lemma f2_ind: ∀A1,A2. ∀f:A1→A2→ℕ. ∀P:relation2 A1 A2.
 @(f2_ind_aux … H) -H [2: // | skip ]
 qed-. 
 
+fact f3_ind_aux: ∀A1,A2,A3. ∀f:A1→A2→A3→ℕ. ∀P:relation3 A1 A2 A3.
+                 (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → P a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → P a1 a2 a3) →
+                 ∀n,a1,a2,a3. f a1 a2 a3 = n → P a1 a2 a3.
+#A1 #A2 #A3 #f #P #H #n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto slow (34s) without #n *)
+qed-.
+
+lemma f3_ind: ∀A1,A2,A3. ∀f:A1→A2→A3→ℕ. ∀P:relation3 A1 A2 A3.
+              (∀n. (∀a1,a2,a3. f a1 a2 a3 < n → P a1 a2 a3) → ∀a1,a2,a3. f a1 a2 a3 = n → P a1 a2 a3) →
+              ∀a1,a2,a3. P a1 a2 a3.
+#A1 #A2 #A3 #f #P #H #a1 #a2 #a3
+@(f3_ind_aux … H) -H [2: // | skip ]
+qed-. 
+
 (* More negated equalities **************************************************)
 
 theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
@@ -596,7 +614,7 @@ pred n - pred m = n - m.
 #n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
 qed.
 
-theorem plus_minus_commutative: ∀x,y,z. z ≤ y → x + (y - z) = x + y - z.
+theorem plus_minus_associative: ∀x,y,z. z ≤ y → x + (y - z) = x + y - z.
 /2 by plus_minus/ qed.
 
 (* More atomic conclusion ***************************************************)
@@ -730,6 +748,9 @@ theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
 <commutative_plus <plus_minus_m_m //
 qed.
 
+lemma minus_minus_associative: ∀x,y,z. z ≤ y → y ≤ x → x - (y - z) = x - y + z.
+/2 width=1 by minus_minus/ qed-.
+
 lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
 /3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
 
@@ -743,6 +764,12 @@ lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
 lemma minus_plus_plus_l: ∀x,y,h. (x + h) - (y + h) = x - y.
 // qed.
 
+lemma plus_minus_plus_plus_l: ∀z,x,y,h. z + (x + h) - (y + h) = z + x - y.
+// qed.
+
+lemma minus_plus_minus_l: ∀x,y,z. y ≤ z → (z + x) - (z - y) = x + y.
+/2 width=1 by minus_minus_associative/ qed-.
+
 (* Stilll more atomic conclusion ********************************************)
 
 (* le *)