proposition: Lemma CReal_mult_proper_l : forall x y z : CReal, y == z -> x * y == x * z.
proof: Proof. intros. apply (CReal_plus_eq_reg_l (-(x*z))). rewrite CReal_plus_opp_l, CReal_opp_mult_distr_r. rewrite <- CReal_mult_plus_distr_l. apply CReal_mult_proper_0_l. rewrite H. apply CReal_plus_opp_l. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra