proposition: Lemma AQsqrt_pos_correct : 'AQsqrt_pos = rational_sqrt ('a).
proof: Proof. unfold AQsqrt_pos. rewrite ARtoCR_preserves_scale, AQsqrt_mid_correct. transitivity (scale (2 ^ Qdlog4 (' a)) (rational_sqrt (' (a ≪ (2 * - Qdlog4 (' a)))))). apply Cmap_wd. rewrite aq_shift_correct, rings.preserves_1, rings.mult_1_l. reflexivity. reflexivity. rewrite aq_shift_correct. rewrite int_pow_exp_mult. apply rational_sqrt_scale. apply semirings.preserves_nonneg. now apply orders.lt_le. 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