proposition: Lemma CReal_mult_0_l : forall r, 0 * r == 0.
proof: Proof. intros. rewrite CReal_mult_comm. apply CReal_mult_0_r. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra