proposition: Lemma CRopp_involutive : forall {R : ConstructiveReals} (r : CRcarrier R), - - r == r.
proof: Proof. intros. apply (CRplus_eq_reg_l (CRopp R r)). transitivity (CR_of_Q R 0). - apply CRisRing. - apply CReq_sym. transitivity (r + - r). + apply CRisRing. + apply CRisRing. Qed.
imports: QArith Qabs Qround