proposition: Lemma AQsqrt_loop_snd_upper_bound (n z : nat) : snd (AQsqrt_loop (z + n)) ≤ (snd (AQsqrt_loop n) + 4) * 2 ^ z - 4.
proof: Proof. induction z; unfold pow; simpl. apply orders.eq_le. ring. revert IHz. case (AQsqrt_loop (z + n)); intros r s IHz. case (decide_rel (≤)); simpl; intros E. rewrite shiftl_1. setoid_replace ((snd (AQsqrt_loop n) + 4) * (2 * 2 ^ z) - 4) with (2 * ((snd (AQsqrt_loop n) + 4) * 2 ^ z - 4 + 2)) by ring. apply (order_preserving (2 *.)). now apply (order_preserving (+2)). rewrite shiftl_1. setoid_replace ((snd (AQsqrt_loop n) + 4) * (2 * 2 ^ z) - 4) with (2 * ((snd (AQsqrt_loop n) + 4) * 2 ^ z - 4 + 2)) by ring. apply (order_preserving (2 *.)). apply semirings.plus_le_compat_r; [solve_propholds | assumption]. 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