proposition: Lemma AQsqrt_loop_invariant2 (n : nat) : fst (AQsqrt_loop n) ≤ 2 * snd (AQsqrt_loop n) + 4.
proof: Proof. induction n; simpl. now setoid_replace (2 * 0 + 4) with 4 by ring. revert IHn; case (AQsqrt_loop n); intros r s IHn. case (decide_rel (≤) (s + 1) r); intros; simpl in *. rewrite shiftl_1, shiftl_2. setoid_replace (2 * (2 * (s + 2)) + 4) with (4 * ((2 * s + 4) - (s + 1))) by ring. apply (order_preserving (4 *.)). now apply (order_preserving (+ _)). rewrite shiftl_1, shiftl_2. setoid_replace (2 * (2 * s) + 4) with (4 * (s + 1)) by ring. apply (order_preserving (4 *.)). now apply orders.le_flip. 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