proposition: Lemma CReal_mult_le_compat_r : forall (r r1 r2:CReal), 0 <= r -> r1 <= r2 -> r1 * r <= r2 * r.
proof: Proof. intros. apply (CReal_plus_le_reg_r (-(r1*r))). rewrite CReal_plus_opp_r, CReal_opp_mult_distr_l. rewrite <- CReal_mult_plus_distr_r. apply CReal_mult_le_0_compat. 2: exact H. apply (CReal_plus_le_reg_r r1). ring_simplify. exact H0. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra