proposition: Lemma AQsqrt_mid_bounded_spec (n : N) : (AQsqrt_mid_bounded_raw n ^ (2%mc:N)) = a - fst (AQsqrt_loop ('n)) ≪ -(2 * 'n).
proof: Proof. unfold AQsqrt_mid_bounded_raw. rewrite shiftl_base_nat_pow, rings.preserves_2. apply (injective (≪ (2 + 2 * 'n))). rewrite shiftl_reverse by ring. rewrite shiftl_base_plus, shiftl_negate, <-shiftl_exp_plus. mc_setoid_replace ((-(2 * 'n) + (2 + 2 * 'n))%mc : Z) with (2%mc : Z) by ring. rewrite shiftl_exp_plus, ?shiftl_2, <-shiftl_mult_l. rewrite <-(rings.preserves_2 (f:=cast N Z)), <-rings.preserves_mult. rewrite shiftl_nat_pow_alt, nat_pow_exp_mult. rewrite (commutativity a), associativity. rewrite <-(preserves_nat_pow_exp (f:=cast N nat) _ n). setoid_replace (2 ^ 2) with 4 by (rewrite nat_pow_2; ring). apply (right_cancellation (+) (4 * fst (AQsqrt_loop (' n)))). rewrite AQsqrt_loop_invariant1. ring. 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