proposition: Lemma rational_sqrt_mid_correct_aux (x : Q) (y : CR) Px : CRpower_N y 2 = 'x → 0%CR ≤ y → y = IRasCR (sqrt (inj_Q IR x) Px).
proof: Proof. intros f_sqrt f_nonneg. rewrite <- (CRasIRasCR_id y). apply IRasCR_wd. assert (X:[0][<=](CRasIR y)[^]2). { apply sqr_nonneg. } stepl (sqrt _ X). - apply sqrt_wd. rewrite -> IR_eq_as_CR. rewrite -> IR_inj_Q_as_CR. simpl. rewrite <- f_sqrt. rewrite <- (CRpower_N_correct 2). simpl. rewrite IR_mult_as_CR, IR_mult_as_CR. rewrite CRasIRasCR_id. rewrite IR_One_as_CR. ring. - apply sqrt_to_nonneg. rewrite -> IR_leEq_as_CR. rewrite -> IR_Zero_as_CR. now rewrite -> CRasIRasCR_id. 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