proposition: Lemma hemiMetric_closed : forall e A b, (forall d, 0 < d -> hemiMetric X (e+d) A (fun a => InFinEnumC a b)) -> hemiMetric X e A (fun a => InFinEnumC a b).
proof: Proof. intros e A b H x Hx. pose (fun n y => ball (e + (1#(P_of_succ_nat n))%Q) x y) as P. assert (forall n, existsC X (fun x => ~~In x b /\ P n x)) as HP. { intros n. unfold P. destruct (H (1#(P_of_succ_nat n))%Q eq_refl x Hx) as [HG | y [Hy0 Hy1]] using existsC_ind. apply existsC_stable; auto. clear - Hy0 Hy1. intro abs. unfold InFinEnumC, FinSubset_ball in Hy0. contradict Hy0; intros [y0 [Hy0 yeq]]. specialize (abs y0). contradict abs. split. intro abs. contradiction. rewrite <- yeq. exact Hy1. } destruct (infinitePidgeonHolePrinicple _ _ P HP) as [HG | y [Hy0 Hy1]] using existsC_ind. apply existsC_stable; auto. apply existsWeaken. exists y. split; auto using InFinEnumC_weaken. apply ball_closed. intros [n d] dpos. destruct n. inversion dpos. 2: inversion dpos. destruct (Hy1 (nat_of_P d)) as [HG | m [Hmd Hm]] using existsC_ind. apply (msp_stable (msp X) (e + (Zpos p#d))%Q); assumption. eapply ball_weak_le;[|apply Hm]. simpl. rewrite -> Qle_minus_iff. ring_simplify. rewrite <- Qle_minus_iff. apply Zmult_le_compat. apply Pos.le_1_l. simpl. apply Pos2Nat.inj_le. apply (Nat.le_trans _ _ _ Hmd). rewrite nat_of_P_o_P_of_succ_nat_eq_succ. apply le_S, Nat.le_refl. discriminate. discriminate. 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