proposition: Lemma rational_sqrt_pos_correct : forall a Ha H, (@rational_sqrt_pos a Ha == IRasCR (sqrt (inj_Q IR a) H))%CR.
proof: Proof. intros a Ha H. unfold rational_sqrt_pos. destruct (Qle_total 1 a). apply rational_sqrt_big_bounded_correct. apply rational_sqrt_small_bounded_correct. 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