-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 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 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. c ≤ a →
- a < b + c → a - c < b.
-#a #b #c #lea #H @not_le_to_lt
-@(not_to_not … (lt_to_not_le …H)) /2/
-qed.
-