#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 ***************************************************)
<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.
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 *)