proposition: Lemma root_step_one_le : forall b, (1 <= b)-> (1 <= root_step b).
proof: Proof. intros b Hb. assert (A0:0<b). apply Qlt_le_trans with 1; auto with *. destruct Ha as [Ha0 Ha1]. unfold root_step. rewrite -> Qle_minus_iff in *. field_simplify (b / (2#1) + a / ((2#1) * b) + -(1));auto with *. apply Qle_shift_div_l. Qauto_pos. ring_simplify. replace RHS with (((b -1) ^ 2 + (a + -(1)))) by simpl; ring. Qauto_nonneg. 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