proposition: Lemma cut_minus_plus_rev_l x y z : y ∸ z = (x + y) ∸ (x + z).
proof: Proof. destruct (total (≤) y z). rewrite !cut_minus_0; intuition. apply (right_cancellation (+) (x + z)). transitivity ((y ∸ z + z) + x); try ring. rewrite !cut_minus_le; try easy; try ring. now apply (order_preserving (x +)). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.minmax