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