proposition: Lemma AQsqrt_mid_bounded_raw_upper_bound (n : N) : AQsqrt_mid_bounded_raw n ≤ 4.
proof: Proof. unfold AQsqrt_mid_bounded_raw. apply (order_reflecting (≪ 1 + 'n)). rewrite shiftl_reverse by ring. etransitivity. rewrite <-(rings.plus_0_r ('n)). now apply AQsqrt_loop_snd_upper_bound. simpl. apply rings.nonneg_minus_compat; [solve_propholds|]. rewrite rings.plus_0_l, shiftl_S. apply semirings.ge_1_mult_le_compat_l. now apply semirings.le_1_2. solve_propholds. apply orders.eq_le. now rewrite shiftl_nat_pow_alt, preserves_nat_pow_exp. 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