proposition: Lemma rational_sqrt_correct : forall a H, (@rational_sqrt a == IRasCR (sqrt (inj_Q IR a) H))%CR.
proof: Proof. intros a H. unfold rational_sqrt. destruct (Qlt_le_dec_fast 0 a). apply rational_sqrt_pos_correct. rewrite <- (IR_nring_as_CR 0). apply IRasCR_wd. simpl. assert (X:[0] [<=] ([0][^]2:IR)). rstepr ([0]:IR). apply leEq_reflexive. stepl (sqrt _ X). apply sqrt_wd. rstepl ([0]:IR). apply leEq_imp_eq. assumption. stepr (inj_Q IR 0); [| now apply (inj_Q_nring IR 0)]. apply inj_Q_leEq. assumption. apply sqrt_to_nonneg. apply leEq_reflexive. 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