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