proposition: Lemma preserves_cut_minus x y : f (x ∸ y) = f x ∸ f y.
proof: Proof. destruct (total (≤) x y) as [E|E]. rewrite (cut_minus_0 x y E), (cut_minus_0 (f x) (f y)). apply rings.preserves_0. now apply (order_preserving _). apply (left_cancellation (+) (f y)). rewrite 2!(commutativity (f y)). rewrite <-rings.preserves_plus. rewrite (cut_minus_le x y E), (cut_minus_le (f x) (f y)). reflexivity. now apply (order_preserving _). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.minmax