proposition: Lemma flip_nonpos_mult_l x y z : z ≤ 0 → x ≤ y → z * y ≤ z * x.
proof: Proof. intros Ez Exy. destruct (decompose_le Ez) as [a [Ea1 Ea2]], (decompose_le Exy) as [b [Eb1 Eb2]]. rewrite Eb2. apply compose_le with (a * b). now apply nonneg_mult_compat. transitivity (z * x + (z + a) * b). rewrite <-Ea2. ring. ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.orders MathClasses.orders.maps