proposition: Lemma cut_minus_mult_distr_l x y z : 0 ≤ x → x * (y ∸ z) = x * y ∸ x * z.
proof: Proof. intros E. destruct (total (≤) y z). rewrite !cut_minus_0; trivial. ring. now apply (maps.order_preserving_nonneg (.*.) x). apply (right_cancellation (+) (x * z)). rewrite <-distribute_l, !cut_minus_le; try easy. now apply (maps.order_preserving_nonneg (.*.) x). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.minmax