proposition: Lemma genball_closed : (∀ (e: Qinf) (a b: X), (∀ d: Qpos, genball (e + d) a b) → genball e a b).
proof: Proof. Proof with auto with *. intros. unfold genball. destruct e... destruct Qdec_sign as [[|]|]. assert (0 < (1#2) * -q)%Q. apply Qmult_lt_0_compat... apply Qopp_Qlt_0_l... pose proof (H2 (exist _ _ H3)). refine (genball_negative _ _ _ _ H4). simpl. ring_simplify. apply Qopp_Qlt_0_l... setoid_replace (- ((1 # 2) * q))%Q with (-q * (1#2))%Q by (simpl; ring). apply Qmult_lt_0_compat... apply Qopp_Qlt_0_l... apply Rclosed. intros. apply ball_genball. apply (H2 d). apply Req. intros. apply ball_genball. assert (d == q + d) by (rewrite q0, Qplus_0_l; reflexivity). apply (genball_Proper d (q+d) H3 a a (reflexivity _) b b (reflexivity _)), H2. 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