X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=6b3a1a19bf7b730af3e90aacec9d36b48a3d0289;hb=bfafdf7d8313ddd24c06d8ce3bba874f780403a9;hp=7ca90dcb27b3e4d49db2dbe7f71e6577adf408b4;hpb=53452958508001e7af3090695b619fe92135fb9e;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 7ca90dcb2..6b3a1a19b 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -913,9 +913,35 @@ theorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m.
   [|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
 qed.
 
+theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
+#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
+qed.
+
 theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
 #n #m #p #lep /2/ qed.
 
+theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
+#a #b #c #H @(le_plus_to_le_r … b) /2/
+qed.
+
+theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
+#a #b #c #H @not_le_to_lt 
+@(not_to_not … (lt_to_not_le …H)) /2/
+qed.
+
+theorem lt_minus_to_plus_r: ∀a,b,c. a < b - c → a + c < b.
+#a #b #c #H @not_le_to_lt @(not_to_not … (le_plus_to_minus …))
+@lt_to_not_le //
+qed.
+
+theorem lt_plus_to_minus: ∀n,m,p. m ≤ n → n < p+m → n-m < p.
+#n #m #p #lenm #H normalize <minus_Sn_m // @le_plus_to_minus //
+qed.
+
+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. 
+
 theorem monotonic_le_minus_r: 
 ∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
 #p #q #n #lepq @le_plus_to_minus
@@ -936,7 +962,7 @@ theorem distributive_times_minus: distributive ? times minus.
   @eq_f (applyS plus_minus_m_m) /2/
 qed.
 
-theorem minus_minus: ∀n,m,p. n-m-p = n -(m+p).
+theorem minus_plus: ∀n,m,p. n-m-p = n -(m+p).
 #n #m #p 
 cases (decidable_le (m+p) n) #Hlt
   [@plus_to_minus @plus_to_minus <associative_plus
@@ -946,6 +972,19 @@ cases (decidable_le (m+p) n) #Hlt
   ]
 qed.
 
+(*
+theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
+#n #m #p #lepm @plus_to_minus >(commutative_plus p)
+>associative_plus <plus_minus_m_m //
+qed.  *)
+
+theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
+  p+(n-m) = n-(m-p).
+#n #m #p #lepm #lemn
+@sym_eq @plus_to_minus <associative_plus <plus_minus_m_m //
+<commutative_plus <plus_minus_m_m //
+qed.
+
 (*********************** boolean arithmetics ********************) 
 include "basics/bool.ma".