x y z : z ≤ 0 -> x ≤ y -> z * y ≤ z * x. 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). - apply nonneg_mult_compat;trivial. - transitivity (z * x + (z + a) * b). + rewrite <-Ea2. rewrite mult_0_l,plus_0_r. reflexivity. + rewrite plus_mult_distr_r,plus_mult_distr_l. apply associativity. Qed.
Require Import