proposition: Lemma root_loop_nonneg : forall (n:nat) q (e:Qpos) (b:Q) (err:positive), 0 <= b -> 0 <= q -> 0 <= root_loop q e n b err.
proof: Proof. induction n. - intros. exact H. - intros. simpl. destruct (Qlt_le_dec_fast (`e) (1#err)). 2: exact H. apply IHn. 2: exact H0. destruct b as [b a]. unfold Qle in H; simpl in H. rewrite Z.mul_1_r in H. destruct q as [q c]. unfold Qle in H0; simpl in H0. rewrite Z.mul_1_r in H0. unfold Qle, Qnum, Qden. rewrite Z.mul_0_l, Z.mul_1_r. rewrite Z.mul_1_r. apply Z_div_pos. reflexivity. apply Z.mul_nonneg_nonneg. 2: discriminate. apply Z.add_nonneg_nonneg. apply Z.mul_nonneg_nonneg. apply H. discriminate. apply Z.mul_nonneg_nonneg. apply Z.mul_nonneg_nonneg. exact H0. 2: discriminate. unfold Qinv, Qmult. simpl. destruct b. discriminate. discriminate. exfalso. apply (Zle_not_lt _ _ H). reflexivity. 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