proposition: Lemma AQsqrt_mid_correct : 'AQsqrt_mid = rational_sqrt ('a).
proof: Proof. apply rational_sqrt_unique. apply semirings.preserves_nonneg. red. transitivity 1; [solve_propholds | intuition]. change ('AQsqrt_mid ^ (2 : N) = cast Q CR (cast AQ Q a)). rewrite <-preserves_nat_pow. rewrite AQsqrt_mid_spec. now apply ARtoCR_inject. change (0%CR) with (0%mc : CR). rewrite <-(rings.preserves_0 (f:=cast AR CR)). apply (order_preserving _). now apply AQsqrt_mid_nonneg. 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