proposition: Lemma ARsqrt_inc : forall x y : AR, ARle 0 x -> ARle x y -> ARle (ARsqrt x) (ARsqrt y).
proof: Proof. intros. apply ARtoCR_preserves_le. rewrite ARtoCR_preserves_sqrt. rewrite ARtoCR_preserves_sqrt. apply CRsqrt_inc. rewrite <- ARtoCR_preserves_0. apply (ARtoCR_preserves_le 0 x), H5. apply (ARtoCR_preserves_le x y), H6. 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