proposition: Lemma CRpi_correct : (IRasCR Pi == CRpi)%CR.
proof: Proof. unfold CRpi. rewrite -> r_pi_correct. apply IRasCR_wd. rstepl ((nring 1)[*]Pi). apply mult_wdl. apply eq_symmetric. apply (inj_Q_nring IR 1). Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.Q_in_CReals CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRarctan_small CoRN.transc.MoreArcTan CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra CoRN.stdlib_omissions.Q