proposition: Lemma root_max_steps : forall (n d:positive), (1#(iter_nat (S (Psize d)) _ (fun x => (x * x)%positive) 2%positive))<= proj1_sig (n#d)%Qpos.
proof: Proof. intros n d. apply Qle_trans with (1#d). clear - d. unfold Qle; simpl. cut ((d <= iter_nat (S (Psize d)) positive (fun x : positive => (x * x)%positive) 2%positive)%Z/\(4 <= iter_nat (S (Psize d)) positive (fun x : positive => (x * x)%positive) 2%positive)%Z). tauto. induction d; split; try discriminate; destruct IHd as [A B]; set (t:=iter_nat (S (Psize d)) positive (fun x : positive => (x * x)%positive) 2%positive) in *. rewrite Zpos_xI. apply Z.le_trans with (4*d)%Z; auto with *. apply (Zmult_le_compat 4 d t t); auto with *. change (4%Z) with (2*2)%Z. apply (Zmult_le_compat 2 2 t t); auto with *. rewrite Zpos_xO. apply Z.le_trans with (4*d)%Z; auto with *. apply (Zmult_le_compat 4 d t t); auto with *. change (4%Z) with (2*2)%Z. apply (Zmult_le_compat 2 2 t t); auto with *. unfold Qle; simpl. change (1*d <= n*d)%Z. auto with *. 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