proposition: Lemma genball_stable : (∀ (e: Q) (a b: X), (~~genball e a b) → genball e a b).
proof: Proof. intros. unfold genball. unfold genball in H2. destruct (Qdec_sign e). destruct s. - contradict H2. intro H2. contradiction. - apply Rstable, H2. - apply Req. unfold equiv in H2. intro d. apply Rstable. intro abs. contradict H2; intro H2. contradict abs. rewrite H2. apply H0. 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