proposition: Lemma FinSubset_ball_closed : forall (e:Q) x l, (forall d:Q, 0 < d -> FinSubset_ball (e+d) x l) -> FinSubset_ball e x l.
proof: Proof. induction l. - intros H. exfalso. exact (FinSubset_ball_nil (H (1#1) eq_refl)). - intros H abs. assert (~ball e x a) as A. { intro H0. contradict abs. exists a. split. left. reflexivity. exact H0. } assert (~ (exists y : X, In y l /\ ball e x y)) as B. { intros [y H1]. contradict abs. exists y. split. right. apply H1. apply H1. } clear abs. revert B. apply IHl. clear IHl. intros d dpos. assert (existsC Qpos (fun d => ~ball (e+proj1_sig d) x a)) as Aprime. { intros Y. apply A. apply ball_closed. intros d0 d0pos. apply (msp_stable (msp X)). apply (Y (exist _ _ d0pos)). } clear A. destruct Aprime as [G | d0 Hd0] using existsC_ind. intro abs; contradict G; intro G; contradiction. intros Z. destruct (Qlt_le_dec (proj1_sig d0) d). + revert Z. apply (@FinSubset_ball_weak_le (e + proj1_sig d0)). apply Qlt_le_weak. rewrite -> Qlt_minus_iff in *. setoid_replace (e + d + - (e + proj1_sig d0)) with (d + - proj1_sig d0) by (simpl; ring). assumption. intros Y. destruct d0 as [d0 d0pos]. apply (H d0 d0pos). intros [y abs]. contradict Y. exists y. simpl. split. 2: apply abs. destruct abs. destruct H0. 2: exact H0. subst y. contradiction. + specialize (H d dpos). unfold FinSubset_ball in H. contradict H; intros [y [iny H]]. destruct iny. subst y. contradict Hd0. apply (@ball_weak_le X (e + d)). rewrite -> Qle_minus_iff in *. setoid_replace (e + proj1_sig d0 + - (e + d)) with (proj1_sig d0 + - d) by (simpl; ring). assumption. exact H. contradict Z. exists y. split. exact H0. exact H. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Hausdorff CoRN.logic.Classic CoRN.stdlib_omissions.List CoRN.metric2.Classification CoRN.metric2.Complete CoRN.metric2.Prelength