proposition: Lemma CRopp_plus_distr : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R), - (r1 + r2) == - r1 + - r2.
proof: Proof. intros. destruct (CRisRing R), (CRisRingExt R). apply (CRplus_eq_reg_l (CRplus R r1 r2)). transitivity (CR_of_Q R 0). 1:apply Ropp_def. transitivity (r2 + r1 + (-r1 + -r2)). 1:transitivity (r2 + (r1 + (-r1 + -r2))). 1:transitivity (r2 + - r2). - apply CReq_sym. apply Ropp_def. - apply Radd_ext. + apply CReq_refl. + transitivity (0 + - r2). * apply CReq_sym, Radd_0_l. * transitivity (r1 + - r1 + - r2). -- apply Radd_ext. 2: apply CReq_refl. apply CReq_sym, Ropp_def. -- apply CReq_sym, Radd_assoc. - apply Radd_assoc. - apply Radd_ext. 2: apply CReq_refl. apply Radd_comm. Qed.
imports: QArith Qabs Qround