proposition: Lemma CR_ap_zero_as_IR : forall x, (IRasCR x >< 0 -> x[#][0])%CR.
proof: Proof. intros x H. apply CR_ap_as_IR. generalize H. apply CRapartT_wd. reflexivity. symmetry. apply IR_Zero_as_CR. 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