proposition: Lemma CRsqrt_sqr : forall (x : CR), (0 <= x -> CRsqrt x * CRsqrt x = x)%CR.
proof: Proof. intros x xpos. rewrite <- (CRasIRasCR_id x). assert ([0] [<=] CRasIR x). { apply IR_leEq_as_CR. rewrite CRasIRasCR_id, IR_Zero_as_CR. exact xpos. } rewrite <- (CRsqrt_correct (CRasIR x) H). rewrite <- IR_mult_as_CR. apply IRasCR_wd. setoid_replace (sqrt (CRasIR x) H [*] sqrt (CRasIR x) H) with (sqrt (CRasIR x) H [^] 2). exact (sqrt_sqr (CRasIR x) H). simpl. destruct (cr_proof IR), ax_mult_mon. rewrite lunit. 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