X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=cca4782806c2264ce0bc294a84bee55881d4a18c;hb=aad5588b82d0f2991c336f7ac2f3fadd76768eeb;hp=bd23c6dd745b49aba23536916462306e4cf265df;hpb=29973426e0227ee48368d1c24dc0c17bf2baef77;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index bd23c6dd7..cca478280 100644
--- 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.
@@ -609,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 ***************************************************)
@@ -743,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.
 
@@ -756,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 *)