proposition: Lemma CRsqrt_correct : forall x H, (IRasCR (sqrt x H) == CRsqrt (IRasCR x))%CR.
proof: Proof. intros x H. assert (X:Dom (FNRoot FId 2 (Nat.lt_0_succ 1)) x). simpl; split; auto. transitivity (IRasCR (FNRoot FId 2 (Nat.lt_0_succ 1) x X)). apply IRasCR_wd. apply: NRoot_wd. apply eq_reflexive. apply (ContinuousCorrect (I:proper (closel [0]))); try assumption. apply Continuous_NRoot. Contin. intros; assumption. intros q Hq Y. transitivity (rational_sqrt q);[|apply: rational_sqrt_correct]. unfold CRsqrt. pose proof (Cbind_correct QPrelengthSpace sqrt_uc). apply ucEq_equiv in H0. rewrite (H0 ('q)%CR). apply BindLaw1. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.Q_in_CReals CoRN.reals.fast.CRpower CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.NRootIR CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.reals.fast.Compress Coq.NArith.Ndigits CoRN.reals.fast.PowerBound CoRN.transc.RealPowers CoRN.reals.fast.ContinuousCorrect CoRN.tactics.Qauto CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra