X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=81d6c9310247dc42c5f2d0d76e66a986ae1d45fc;hb=1f946a70bc439ced80c695f0fd0c210df0d3b767;hp=56482a0428e6e434a880d23d9f4dcd9f042e0c9c;hpb=433a742bd425848f273c7faf192c96a51ab9d8c5;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 56482a042..81d6c9310 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -1,4 +1,4 @@
-  (*
+(*
     ||M||  This file is part of HELM, an Hypertextual, Electronic        
     ||A||  Library of Mathematics, developed at the Computer Science     
     ||T||  Department of the University of Bologna, Italy.                     
@@ -132,6 +132,9 @@ theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
 theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
 #n (elim n) normalize /3/ qed.
 
+theorem injective_plus_l: ∀n:nat.injective nat nat (λm.m+n). 
+/2/ qed.
+
 theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
 /2/ qed.
 
@@ -184,6 +187,9 @@ theorem minus_Sn_n: ∀n:nat. S 0 = (S n)-n.
 theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
 @nat_elim2 normalize // qed.
 
+lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
+// qed.
+
 (* Negated equalities *******************************************************)
 
 theorem not_eq_O_S : ∀n:nat. 0 ≠ S n.
@@ -368,6 +374,13 @@ theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b.
 #a #b #c #H @le_plus_to_minus_r //
 qed.
 
+lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + (S n).
+/2 width=1/ qed.
+
+theorem lt_S_S_to_lt: ∀n,m:nat. S n < S m → n < m.
+(* demo *)
+/2/ qed-.
+
 (* not le, lt *)
 
 theorem not_le_Sn_O: ∀ n:nat. S n ≰ 0.
@@ -427,8 +440,26 @@ theorem increasing_to_le2: ∀f:nat → nat. increasing f →
   ]
 qed.
 
+lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
+/3 width=2/ qed-.
+
+lemma lt_inv_plus_l: ∀x,y,z. x + y < z → x < z ∧ y < z - x.
+/3 width=2/ qed-.
+
+lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
+#m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/
+qed-.
+
+lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
+#m #n elim (decidable_le m n) /2 width=1/ /4 width=2/
+qed-.
+
 (* More general conclusion **************************************************)
 
+theorem nat_ind_plus: ∀R:predicate nat.
+                      R 0 → (∀n. R n → R (n + 1)) → ∀n. R n.
+/3 width=1 by nat_ind/ qed-.
+
 theorem lt_O_n_elim: ∀n:nat. 0 < n → 
   ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
 #n (elim n) // #abs @False_ind /2/ @absurd
@@ -519,6 +550,9 @@ 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.
+/2 by plus_minus/ qed.
+
 (* More atomic conclusion ***************************************************)
 
 (* le *)
@@ -561,6 +595,9 @@ theorem increasing_to_le: ∀f:nat → nat.
 @(ex_intro ?? (S a)) /2/
 qed.
 
+lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 ≤ y1 + y2.
+/3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed.
+
 (* lt *)
 
 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
@@ -630,7 +667,28 @@ theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
 <commutative_plus <plus_minus_m_m //
 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.
+
+lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
+#b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); //
+qed.
+
+lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
+/2 width=1/ qed.
+
+(* Stilll more atomic conclusion ********************************************)
+
+(* le *)
+
+lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
+#m1 #m2 #H #n1 #n2 >commutative_plus
+#H elim (le_inv_plus_l … H) -H >commutative_plus <minus_le_minus_minus_comm //
+#H #_ @(transitive_le … H) /2 width=1/
+qed-. 
+
 (*********************** boolean arithmetics ********************) 
+
 include "basics/bool.ma".
 
 let rec eqb n m ≝ 
@@ -700,10 +758,10 @@ theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
 
 (* min e max *)
 definition min: nat →nat →nat ≝
-λn.λm. if_then_else ? (leb n m) n m.
+λn.λm. if leb n m then n else m.
 
 definition max: nat →nat →nat ≝
-λn.λm. if_then_else ? (leb n m) m n.
+λn.λm. if leb n m then m else n.
 
 lemma commutative_min: commutative ? min.
 #n #m normalize @leb_elim 
@@ -736,4 +794,3 @@ lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
 lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
 #i #n #m #leni #lemi normalize (cases (leb n m)) 
 normalize // qed.
-