-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 elim b -b
-[ #c #a #H >(le_n_O_to_eq … H) -H //
-| #b #IHb #c elim c -c //
- #c #_ #a #Hcb
- lapply (le_S_S_to_le … Hcb) -Hcb #Hcb
- <plus_n_Sm normalize /2 width=1/
-]
-qed.
-