proposition: Lemma CR_of_Q_opp : forall {R : ConstructiveReals} (q : Q), CR_of_Q R (-q) == - CR_of_Q R q.
proof: Proof. intros. apply (CRplus_eq_reg_l (CR_of_Q R q)). transitivity (CR_of_Q R 0). - transitivity (CR_of_Q R (q-q)). + apply CReq_sym, CR_of_Q_plus. + apply CR_of_Q_morph. ring. - apply CReq_sym. apply (CRisRing R). Qed.
imports: QArith Qabs Qround