proposition: Lemma AQsqrt_mid_bounded_regular_aux1 (n m : N) : m ≤ n → AQsqrt_mid_bounded_raw n - AQsqrt_mid_bounded_raw m ≤ 1 ≪ (1 - 'm : Z).
proof: Proof. intros E. apply naturals.nat_le_plus in E. destruct E as [z E]. rewrite commutativity in E. change (n ≡ z + m) in E. subst. unfold AQsqrt_mid_bounded_raw. rewrite rings.preserves_plus. etransitivity. apply semirings.plus_le_compat; [| reflexivity]. apply (order_preserving (≪ _)). etransitivity. now apply AQsqrt_loop_snd_upper_bound. apply rings.nonneg_minus_compat; [solve_propholds | reflexivity]. apply orders.eq_le. rewrite <-(shiftl_nat_pow_alt (f:=cast nat Z)). rewrite (naturals.to_semiring_twice _ _ (cast N Z)). rewrite <-shiftl_exp_plus, rings.preserves_plus. mc_setoid_replace (('z - (1 + ('z + 'm)))%mc : Z) with ((-(1 + 'm))%mc : Z) by ring. rewrite shiftl_base_plus. ring_simplify. mc_setoid_replace ((1 - ' m)%mc : Z) with ((2 - (1 + 'm))%mc : Z) by ring. now rewrite shiftl_exp_plus, shiftl_2, rings.mult_1_r. 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