proposition: Lemma ARsqrt_srq_abs : forall x : AR, ARsqrt (x*x) = ARabs x.
proof: Proof. assert (forall x : AR, ARle 0 x -> ARsqrt (x*x) = ARabs x) as posCase. { intros. rewrite ARsqrt_mult, ARsqrt_correct. rewrite ARabs_pos. reflexivity. exact H5. exact H5. exact H5. exact H5. } intros. apply ball_stable. intro abs. assert (~(ARle 0 x)). - intro H5. contradict abs. apply posCase, H5. - contradict H5. apply ARle_not_lt. intro H5. contradict abs. change (ARsqrt (x*x) = ARabs x). rewrite <- ARabs_opp. setoid_replace (x * x) with (-x * -x) by ring. apply posCase. destruct (ARtoCR_preserves_ltT x 0) as [c _]. specialize (c H5). apply ARtoCR_preserves_le. rewrite ARtoCR_preserves_0. rewrite <- CRopp_0. rewrite ARtoCR_preserves_opp. apply CRopp_le_compat. rewrite <- ARtoCR_preserves_0. apply CRlt_le_weak, c. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.setoid_ring.Ring CoRN.stdlib_omissions.Z CoRN.model.totalorder.QposMinMax CoRN.metric2.Complete CoRN.model.metric2.Qmetric Coq.ZArith.ZArith CoRN.util.Qdlog CoRN.reals.fast.CRroot CoRN.reals.faster.ARabs MathClasses.interfaces.abstract_algebra MathClasses.theory.shiftl MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.reals.faster.ARArith CoRN.metric2.MetricMorphisms