proposition: Lemma genball_alt (q: Q) (x y: X): genball q x y <-> match Qdec_sign q with | inl (inl _) => False | inl (inr p) => genball q x y | inr _ => x=y end.
proof: Proof. unfold genball. simpl. split; destruct Qdec_sign as [[|]|]; auto. 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