x y z : z < 0 -> x < y -> z * y < z * x. Proof. intros Ez Exy. destruct (decompose_lt Ez) as [a [Ea1 Ea2]], (decompose_lt Exy) as [b [Eb1 Eb2]]. rewrite Eb2. apply compose_lt with (a * b). - apply pos_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