proposition: Lemma CRsquare_nonneg_cancel : forall x y : CR, (0 <= x)%CR -> (0 <= y)%CR -> msp_eq (x*x)%CR (y*y)%CR -> msp_eq x y.
proof: Proof. intros. assert (msp_eq ((x-y)*(x+y))%CR 0%CR). { rewrite (CRplus_eq_l (y*y)%CR). ring_simplify. exact H1. } apply ball_stable. intro abs. apply CRmult_eq_0_reg_l in H2. contradict abs. rewrite (CRplus_eq_l (-y)%CR x y). rewrite CRplus_opp. exact H2. intro H3. assert (msp_eq x 0%CR). { apply CRle_antisym. split. 2: exact H. rewrite <- CRplus_0_r. apply (@CRle_trans _ (x+y)%CR). apply CRplus_le_l. exact H0. rewrite H3. apply CRle_refl. } rewrite H4, CRplus_0_l in H3. contradict abs. rewrite H3, H4. 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