proposition: Lemma CReal_mult_eq_reg_r : forall r r1 r2, r1 * r == r2 * r -> r # 0 -> r1 == r2.
proof: Proof. intros. apply (CReal_mult_eq_reg_l r). - exact H0. - now rewrite 2!(CReal_mult_comm r). Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra