proposition: Lemma rational_sqrt_big_bounded_correct : forall n a Ha H, (@rational_sqrt_big_bounded n a Ha == IRasCR (sqrt (inj_Q IR a) H))%CR.
proof: Proof. induction n. intros a Ha H. simpl. rewrite <- IR_inj_Q_as_CR. apply IRasCR_wd. assert (X:[0][<=](inj_Q IR 1:IR)[^]2) by apply sqr_nonneg. stepl (sqrt _ X). apply sqrt_wd. rstepl (inj_Q IR 1[*]inj_Q IR 1). stepl (inj_Q IR (1*1)); [| now apply (inj_Q_mult IR)]. apply inj_Q_wd. simpl. rewrite -> Qeq_le_def. assumption. apply sqrt_to_nonneg. stepr (nring 1:IR); [| now (apply eq_symmetric; apply (inj_Q_nring IR 1))]. rstepr ([1]:IR). apply less_leEq; apply pos_one. intros a Ha H. simpl. destruct (Qle_total a). apply rational_sqrt_mid_correct. change (scale 2 (rational_sqrt_big_bounded n (a / 4%positive)(rational_sqrt_big_bounded_subproof0 n a Ha q)) == IRasCR (sqrt (inj_Q IR a) H))%CR. assert (X:[0][<=]inj_Q IR (a/4%positive)). change (a/4%positive) with (a*(1#4)). stepr (inj_Q IR a[*]inj_Q IR (1#4)); [| now apply eq_symmetric; apply (inj_Q_mult IR)]. apply mult_resp_nonneg. assumption. stepl (inj_Q IR 0); [| now (apply (inj_Q_nring IR 0))]. apply inj_Q_leEq. discriminate. set (X0:= (rational_sqrt_big_bounded_subproof0 n a Ha q)). rewrite -> (IHn (a/4%positive) X0 X). apply rational_sqrt_big_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