proposition: Lemma AQsqrt_loop_fst_upper_bound (n : nat) : fst (AQsqrt_loop n) ≤ 2 ^ (3 + n).
proof: Proof. Proof with auto. transitivity (2 * snd (AQsqrt_loop n) + 4). apply AQsqrt_loop_invariant2. change (2 ^ (3 + n)) with (2 * (2 * (2 * 2 ^ n))). setoid_replace (2 * snd (AQsqrt_loop n) + 4) with (2 * (snd (AQsqrt_loop n) + 2)) by ring. apply (order_preserving (2 *.)). setoid_replace (2 * (2 * 2 ^ n)) with ((4 * 2 ^ n - 2) + 2) by ring. apply (order_preserving (+ 2)). transitivity (4 * 2 ^ n - 4). rewrite <-(rings.plus_0_r n) at 1. rewrite <-(rings.plus_0_l 4) at 1. now apply AQsqrt_loop_snd_upper_bound. apply semirings.plus_le_compat. now rewrite commutativity. now apply rings.flip_le_negate, semirings.le_2_4. 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