X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=cca4782806c2264ce0bc294a84bee55881d4a18c;hb=3bf7a0b4185dbffe5b822c907956acdbe2d1c559;hp=8613043b8d70c0705af03428371be11ea63b3a1d;hpb=bec531b57a008238f67cd72edc751844d28b374f;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 8613043b8..cca478280 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -614,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 ***************************************************)
@@ -748,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.
 
@@ -761,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 *)