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). - 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.
imports: HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.orders HoTT.Classes.orders.maps