proposition: Lemma CRplus_opp_l : forall {R : ConstructiveReals} (x : CRcarrier R), - x + x == 0.
proof: Proof. intros. destruct (CRisRing R). transitivity (x + - x). - apply Radd_comm. - apply Ropp_def. Qed.
imports: QArith Qabs Qround