proposition: Lemma root_loop_one_le : forall e n b err, (1 <= b)-> (1 <= root_loop e n b err).
proof: Proof. intros e n. induction n; auto with *. simpl. intros b err Hb. destruct (Qlt_le_dec_fast (proj1_sig e) (1 # err)) as [A|A]; try assumption. apply IHn. apply approximateQ_big. apply root_step_one_le. assumption. 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