proposition: Lemma CRplus_eq_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), r + r1 == r + r2 -> r1 == r2.
proof: Proof. intros. destruct (CRisRingExt R). clear Rmul_ext Ropp_ext. pose proof (Radd_ext (CRopp R r) (CRopp R r) (CReq_refl _) _ _ H). destruct (CRisRing R). apply (CReq_trans r1) in H0. - apply (CReq_trans _ _ _ H0). transitivity ((- r + r) + r2). + apply Radd_assoc. + transitivity (0 + r2). * apply Radd_ext. -- apply CRplus_opp_l. -- apply CReq_refl. * apply Radd_0_l. - apply CReq_sym. transitivity (- r + r + r1). + apply Radd_assoc. + transitivity (0 + r1). * apply Radd_ext. -- apply CRplus_opp_l. -- apply CReq_refl. * apply Radd_0_l. Qed.
imports: QArith Qabs Qround