proposition: Lemma CRsquare_pos : forall x : CR, (0 <= x*x)%CR.
proof: Proof. intros x. apply CRle_not_lt. intro abs. assert (~(0 <= x)%CR) as H. { intro J. revert abs. apply CRle_not_lt. exact (CRmult_le_0_compat x x J J). } contradict H. apply CRle_not_lt. intro H. revert abs. apply CRle_not_lt. apply CRlt_le_weak in H. setoid_replace (x*x)%CR with (-x*-x)%CR by (unfold equiv, msp_Equiv; ring). apply CRmult_le_0_compat. rewrite <- CRopp_0. apply CRopp_le_compat, H. rewrite <- CRopp_0. apply CRopp_le_compat, H. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders