proposition: Lemma CRplus_eq_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), r1 + r == r2 + r -> r1 == r2.
proof: Proof. intros. apply (CRplus_eq_reg_l r). transitivity (r1 + r). - apply (Radd_comm (CRisRing R)). - transitivity (r2 + r). + exact H. + apply (Radd_comm (CRisRing R)). Qed.
imports: QArith Qabs Qround