proposition: Lemma genball_negative (q: Q): (q < 0)%Q → ∀ x y: X, ~ genball q x y.
proof: Proof. Proof with auto. unfold genball. intros E ??. destruct Qdec_sign as [[|]|U]; intro... apply (Qlt_is_antisymmetric_unfolded 0 q)... revert E. rewrite U. apply Qlt_irrefl. 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