proposition: Lemma sqrt_raw_nonneg : forall a e, 0 <= a -> 0 <= sqrt_raw a e.
proof: Proof. intros. destruct e. 2: discriminate. simpl. destruct (Qlt_le_dec_fast (`q) (1#2)). apply root_loop_nonneg. rewrite Z.mul_1_r, Z.mul_1_r. destruct a as [a b]; simpl. destruct a. - simpl. unfold Qle; simpl. rewrite Z.mul_1_r. apply Z.div_pos. discriminate. reflexivity. - simpl. unfold Qle, Qnum, Qden. rewrite Z.mul_0_l, Z.mul_1_r. apply Z.div_pos. 2: reflexivity. discriminate. - exfalso. unfold Qle in H; simpl in H. apply (Zle_not_lt _ _ H). reflexivity. - exact H. - unfold initial_root. apply Qmult_le_0_compat. discriminate. apply (Qle_trans _ (0+1)). discriminate. apply Qplus_le_l, H. 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