proposition: Lemma CReal_mult_le_compat_l : forall (r r1 r2:CReal), 0 <= r -> r1 <= r2 -> r * r1 <= r * r2.
proof: Proof. intros. apply (CReal_plus_le_reg_r (-(r*r1))). rewrite CReal_plus_opp_r, CReal_opp_mult_distr_r. rewrite <- CReal_mult_plus_distr_l. apply CReal_mult_le_0_compat. { exact H. } apply (CReal_plus_le_reg_r r1). rewrite CReal_plus_0_l, CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_r. exact H0. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra