proposition: Lemma AQsqrt_mid_nonneg : 0 ≤ AQsqrt_mid.
proof: Proof. intros ε. transitivity (0 : Q). apply rings.flip_nonneg_negate. now apply orders.lt_le, Qpos_ispos. change ((0:Q) ≤ '(AQsqrt_mid_raw ((1#2) * ε) - 0)). apply semirings.preserves_nonneg, rings.flip_nonneg_minus. now apply AQsqrt_mid_bounded_raw_lower_bound. 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