proposition: Lemma CRmult_eq_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), r ≶ 0 -> r * r1 == r * r2 -> r1 == r2.
proof: Proof. intros. rewrite (Rmul_comm (CRisRing R)) in H0. rewrite (Rmul_comm (CRisRing R) r) in H0. apply CRmult_eq_reg_r in H0. - exact H0. - destruct H. + right. exact c. + left. exact c. Qed.
imports: QArith Qabs Qround