proposition: Lemma CReal_mult_lt_compat_l : forall x y z : CReal, 0 < x -> y < z -> x*y < x*z.
proof: Proof. intros. apply (CReal_plus_lt_reg_l (CReal_opp (CReal_mult x y))). rewrite CReal_plus_comm. pose proof CReal_plus_opp_r. unfold CReal_minus in H1. rewrite H1. rewrite CReal_mult_comm, CReal_opp_mult_distr_l, CReal_mult_comm. rewrite <- CReal_mult_plus_distr_l. apply CReal_mult_lt_0_compat. - exact H. - apply (CReal_plus_lt_reg_l y). rewrite CReal_plus_comm, CReal_plus_0_l. rewrite <- CReal_plus_assoc, H1, CReal_plus_0_l. exact H0. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra