proposition: Lemma AQsqrt_mid_bounded_regular_aux2 (n m : N) : n ≤ m → AQsqrt_mid_bounded_raw n ≤ AQsqrt_mid_bounded_raw m.
proof: Proof. intros E. apply naturals.nat_le_plus in E. destruct E as [z E]. rewrite commutativity in E. change (m ≡ z + n) in E. subst. unfold AQsqrt_mid_bounded_raw. rewrite 2!rings.preserves_plus. mc_setoid_replace ((-(1 + 'n))%mc : Z) with (('z - (1 + ('z + 'n)))%mc : Z) by ring. rewrite shiftl_exp_plus. apply (order_preserving (≪ _)). rewrite shiftl_nat_pow_alt, <-(preserves_nat_pow_exp (f:=cast N nat)). now apply AQsqrt_loop_snd_lower_bound. 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