proposition: Lemma cut_minus_0_plus_toggle x : x + (0 ∸ x) = x ∸ 0.
proof: Proof. destruct (total (≤) 0 x). rewrite (cut_minus_0 0 x), (cut_minus_nonneg_0_r x) by easy. ring. rewrite (cut_minus_0 x 0), commutativity; auto. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.minmax