proposition: Lemma FinEnum_ball_eq : forall a b : list X, (forall e : Qpos, FinEnum_ball (proj1_sig e) a b) -> FinEnum_eq a b.
proof: Proof. unfold FinEnum_ball, FinEnum_eq. cut (forall a b : list X, (forall e : Qpos, hemiMetric X (proj1_sig e) (fun a0 : X => InFinEnumC a0 a) (fun a0 : X => InFinEnumC a0 b)) -> forall x : X, InFinEnumC x a -> InFinEnumC x b). { unfold hausdorffBall. split; apply H; firstorder. } induction a. intros. exfalso. unfold InFinEnumC, FinSubset_ball in H0. contradict H0; intros [y [H0 _]]. contradiction. intros b H x Hx. intro abs. unfold InFinEnumC, FinSubset_ball in Hx. contradict Hx; intros [y [iny Hx]]. destruct iny. - subst y. assert (H':forall n :nat , existsC X (fun y : X => InFinEnumC y b /\ ball (m:=X) (1#(P_of_succ_nat n)) x y)). { intros e. apply (H (exist (Qlt 0) (1#(P_of_succ_nat e)) eq_refl)). intro H0. contradict H0. exists a. split. left. reflexivity. exact Hx. } assert (H'':forall n :nat , existsC X (fun y : X => ~~In y b /\ ball (m:=X) (1#(P_of_succ_nat n)) x y)). { intros n. destruct (H' n) as [HG | z [Hz0 Hz1]] using existsC_ind. auto using existsC_stable. clear - Hz1 Hz0. intro abs. unfold InFinEnumC, FinSubset_ball in Hz0. contradict Hz0; intros [y [iny Hz0]]. specialize (abs y). contradict abs. split. intro abs. contradiction. rewrite <- Hz0. exact Hz1. } destruct (infinitePidgeonHolePrinicple _ _ _ H'') as [HG | y [Hy0 Hy1]] using existsC_ind. contradict HG. intro HG. contradiction. revert abs. change (FinSubset_ball 0 x b). rewrite -> (FinSubset_ball_wd x y). 2: reflexivity. apply InFinEnumC_weaken, Hy0. apply ball_eq. intros [n d] dpos. destruct n. inversion dpos. 2: inversion dpos. replace d with (Pos.of_succ_nat (Init.Nat.pred (Pos.to_nat d))). destruct (Hy1 (pred (nat_of_P d))) as [HG | z [Hz0 Hz1]] using existsC_ind. apply (msp_stable (msp X) (Zpos p # Pos.of_succ_nat (Init.Nat.pred (Pos.to_nat d)))). auto. apply ball_weak_le with (1 # P_of_succ_nat z); auto. simpl. apply Zmult_le_compat; [..|auto with *]. apply Pos.le_1_l. simpl. assert (forall i j:nat, le i j -> Pos.of_succ_nat i <= Pos.of_succ_nat j)%positive. { intros. rewrite Pos.of_nat_succ, Pos.of_nat_succ. apply Pos2Nat.inj_le. rewrite Nat2Pos.id, Nat2Pos.id. apply le_n_S, H0. discriminate. discriminate. } apply H0, Hz0. discriminate. rewrite Pos.of_nat_succ. rewrite <- (Pos2Nat.id d) at 2. apply f_equal. apply (Nat.lt_succ_pred O _). apply Pos2Nat.is_pos. - revert abs. apply IHa. intros e y0 Hy. apply H. intro abs. unfold InFinEnumC, FinSubset_ball in Hy. contradict Hy; intros [y1 Hy]. contradict abs. exists y1. split. right. apply Hy. apply Hy. intro abs; contradict abs. exists y. split; assumption. 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