proposition: Lemma rational_sqrt_big_bounded_correct_aux a Xa4 Xa : ((scale (2#1)) (IRasCR (sqrt (inj_Q IR (a / (4#1))) Xa4)) == IRasCR (sqrt (inj_Q IR a) Xa))%CR.
proof: Proof. rewrite <- CRmult_scale. rewrite <- IR_inj_Q_as_CR. rewrite <- IR_mult_as_CR. apply IRasCR_wd. assert (X1:[0][<=](inj_Q IR (4#1))). stepl (inj_Q IR 0); [| now (apply (inj_Q_nring IR 0))]. apply inj_Q_leEq. discriminate. csetoid_replace (inj_Q IR (2#1)) (sqrt _ X1). assert (X2:[0][<=](inj_Q IR (4#1)[*]inj_Q IR (a/4%positive))). apply mult_resp_nonneg;assumption. astepl (sqrt _ X2). apply sqrt_wd. csetoid_rewrite_rev (inj_Q_mult IR (4#1) (a/4%positive)). apply inj_Q_wd. simpl. field; discriminate. change (inj_Q IR (4#1)) with (inj_Q IR ((2#1)[*](2#1))). assert (X2:[0][<=](inj_Q IR (2#1))[^]2). apply sqr_nonneg. stepr (sqrt _ X2). apply eq_symmetric; apply sqrt_to_nonneg. stepl (inj_Q IR 0); [| now (apply (inj_Q_nring IR 0))]. apply inj_Q_leEq. discriminate. apply sqrt_wd. rstepl ((inj_Q IR (2#1))[*](inj_Q IR (2#1))). apply eq_symmetric. apply (inj_Q_mult IR (2#1) (2#1)). 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