proposition: Lemma cut_minus_plus_toggle2 x y z : y ≤ x → y ≤ z → (x ∸ z) + (z ∸ y) = (z ∸ x) + (x ∸ y).
proof: Proof. intros. destruct (total (≤) x z). rewrite (cut_minus_0 x z), cut_minus_le_trans by easy. ring. rewrite (cut_minus_0 z x) by easy. ring_simplify. now auto. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.minmax