proposition: Lemma ARsqrt_correct : forall (x : AR), ARle 0 x -> ARsqrt x * ARsqrt x = x.
proof: Proof. intros x xpos. apply (injective (Eembed QPrelengthSpace (cast AQ Q_as_MetricSpace))). change (Eembed QPrelengthSpace (cast AQ Q_as_MetricSpace) x) with ('x). change (Eembed QPrelengthSpace (cast AQ Q_as_MetricSpace) (ARsqrt x * ARsqrt x)) with ('(ARsqrt x * ARsqrt x)). rewrite (ARtoCR_preserves_mult (ARsqrt x) (ARsqrt x)). rewrite ARtoCR_preserves_sqrt. apply CRsqrt_sqr. rewrite <- ARtoCR_preserves_0. apply (ARtoCR_preserves_le 0 x), xpos. 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