proposition: Lemma CRsqrt_inc : forall x y : CR, (0 <= x -> x <= y -> CRsqrt x <= CRsqrt y)%CR.
proof: Proof. intros. apply (CRplus_le_r _ _ (-CRsqrt x)%CR). rewrite CRplus_opp. apply CRle_not_lt. intro abs. assert ((0 < y)%CR -> False). { intro ypos. revert abs. apply CRle_not_lt. apply (CRmult_le_0_reg_l (CRsqrt x + CRsqrt y)%CR). - intro abs. apply CRle_not_lt in abs. assert (msp_eq 0%CR (CRsqrt y)). apply CRle_antisym. split. apply CRsqrt_pos. apply CRlt_le_weak, ypos. rewrite <- CRplus_0_l. refine (CRle_trans _ abs). apply CRplus_le_r, CRsqrt_pos, H. pose proof (CRmult_wd H1 H1) as H3. rewrite CRmult_0_r, CRsqrt_sqr in H3. apply CRle_antisym in H3. revert ypos. apply CRle_not_lt, H3. apply CRlt_le_weak, ypos. - setoid_replace ((CRsqrt x + CRsqrt y) * (CRsqrt y + (- CRsqrt x)))%CR with (CRsqrt y*CRsqrt y - (CRsqrt x*CRsqrt x))%CR by ring. rewrite (CRsqrt_sqr y). rewrite (CRsqrt_sqr x). rewrite <- (CRplus_opp x). apply CRplus_le_r, H0. exact H. exact (CRle_trans H H0). } apply CRle_not_lt in H1. revert abs. apply CRle_not_lt. setoid_replace x with 0%CR. setoid_replace y with 0%CR. rewrite CRplus_opp. apply CRle_refl. apply CRle_antisym. split. exact H1. exact (CRle_trans H H0). apply CRle_antisym. split. exact (CRle_trans H0 H1). exact 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