proposition: Lemma CRsqrt_mult : forall x y, (0 <= x -> 0 <= y -> CRsqrt (x*y) = CRsqrt x * CRsqrt y)%CR.
proof: Proof. intros x y xpos ypos. apply (CRsquare_nonneg_cancel (CRsqrt (x*y)%CR) (CRsqrt x * CRsqrt y)%CR (CRsqrt_pos _ (CRmult_le_0_compat _ _ xpos ypos))). apply CRmult_le_0_compat; apply CRsqrt_pos; assumption. rewrite CRsqrt_sqr. 2: exact (CRmult_le_0_compat _ _ xpos ypos). transitivity (CRsqrt x * CRsqrt x * (CRsqrt y * CRsqrt y))%CR. 2: ring. rewrite CRsqrt_sqr, CRsqrt_sqr. reflexivity. exact ypos. exact xpos. 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