proposition: Lemma AQsqrt_loop_snd_nonneg (n : nat) : 0 ≤ snd (AQsqrt_loop n).
proof: Proof. rewrite <-(rings.plus_0_r n) at 1. etransitivity. 2: apply AQsqrt_loop_snd_lower_bound. simpl. apply orders.eq_le. ring. 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