proposition: Lemma rational_sqrt_big_bounded_nonneg : forall n (a:Q) Ha e, 0 <= approximate (rational_sqrt_big_bounded n a Ha) e.
proof: Proof. induction n. - intros. discriminate. - intros. simpl. destruct (Qle_total a (4#1)). + simpl. apply (sqrt_raw_nonneg a e). destruct Ha. apply (Qle_trans _ 1). discriminate. exact H. + unfold Cmap_fun; simpl. rewrite <- (Qmult_0_r (2#1)). apply Qmult_le_l. reflexivity. apply IHn. 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