proposition: Lemma rational_sqrt_small_bounded_correct : forall n a Ha H, (@rational_sqrt_small_bounded n a Ha == IRasCR (sqrt (inj_Q IR a) H))%CR.
proof: Proof. induction n; try apply rational_sqrt_mid_correct. intros a Ha H. simpl. destruct (Qle_total a 1); [| apply rational_sqrt_mid_correct]. change (scale (1#2) (rational_sqrt_small_bounded n (4%positive*a) (rational_sqrt_small_bounded_subproof n a Ha q)) == IRasCR (sqrt (inj_Q IR a) H))%CR. assert (X:[0][<=]inj_Q IR (4%positive*a)). stepr (inj_Q IR (4%positive:Q)[*]inj_Q IR a); [| now apply eq_symmetric; apply (inj_Q_mult IR)]. apply mult_resp_nonneg. stepl (inj_Q IR 0); [| now (apply (inj_Q_nring IR 0))]. apply inj_Q_leEq. discriminate. assumption. set (X0:= (rational_sqrt_small_bounded_subproof n a Ha q)). rewrite -> (IHn (4%positive*a) X0 X). apply rational_sqrt_small_bounded_correct_aux. 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