proposition: Lemma CRasIRasCR_id : forall (x:CR), (IRasCR (CRasIR x)==x)%CR.
proof: Proof. apply (inversity_rht _ _ CRIR_iso). Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.CauchySeq CoRN.reals.iso_CReals CoRN.reals.R_morphism CoRN.reals.fast.CRArith CoRN.model.reals.CRreal CoRN.tactics.CornTac