proposition: Lemma genball_Reflexive (q: Qinf): (0 <= q)%Qinf → Reflexive (genball q).
proof: Proof. Proof with auto. repeat intro. unfold genball. destruct q... destruct Qdec_sign as [[|]|]; intuition... apply (Qlt_not_le q 0)... Qed.
imports: CoRN.algebra.RSetoid Arith List CoRN.model.totalorder.QposMinMax CSetoids Qmetric Qring Qinf QnnInf QnonNeg ProductMetric QposInf Qposclasses UniformContinuity MathClasses.implementations.stdlib_rationals stdlib_omissions.Pair stdlib_omissions.Q PointFree MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.theory.products