proposition: Lemma rational_sqrt_mid_le_3 : forall (e:QposInf), (approximate rational_sqrt_mid e) <= 3.
proof: Proof. intros [e|];[|discriminate]. change (sqrt_raw e <= (3#1)). unfold sqrt_raw. set (n:= (S (Psize (Qden (proj1_sig e))))). assert (root_has_error (Qpos_min (1 # 2) e) (root_loop e n initial_root 2)). apply root_loop_error. apply initial_root_one_le. apply initial_root_error. subst n. clear. revert e. intros [[n d] epos]. destruct n as [|n|n]. inversion epos. 2: inversion epos. apply root_max_steps. eapply Qle_trans. apply root_error_bnd;[| |apply H]. eapply Qle_trans. apply Qpos_min_lb_l. discriminate. apply root_loop_one_le. apply initial_root_one_le. rewrite Q_Qpos_min. simpl. apply (Qle_trans _ (2 + (1#2))). apply Qplus_le_r, Qmin_lb_l. discriminate. 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