proposition: Lemma HemiMetricHemiMetricStrong : forall (e:Q) A b, hemiMetric X e A (fun a => InFinEnumC a b) -> hemiMetricStrong X e A (fun a => InFinEnumC a b).
proof: Proof. intros e A b H x Hx. generalize (H x Hx). clear H. revert x Hx. induction b; intros x Hx H d. - abstract (unfold existsC in H; contradict H; intros y [H _]; exact (FinSubset_ball_nil H)). - destruct (@almostDecideX e (e + proj1_sig d) x a). clear - e d. abstract ( simpl; rewrite -> Qlt_minus_iff; ring_simplify; auto with * ). exists a. clear - b0. abstract (auto using InFinEnumC_weaken with * ). assert (Z:existsC X (fun y : X => InFinEnumC y b /\ ball (m:=X) e x y)). { clear - H n. destruct (H) as [HG | y [Hy0 Hy1]] using existsC_ind. auto using existsC_stable. apply existsWeaken. exists y. split. 2: exact Hy1. apply FinSubset_ball_orC in Hy0. destruct Hy0 as [HG | Hy | Hy] using orC_ind. intro abs. contradict HG; intro HG; contradiction. 2: assumption. apply (ball_wd _ eq_refl _ _ (reflexivity _) _ _ Hy) in Hy1. contradiction. } exists (let (y,_) := (IHb x Hx Z d) in y). clear - IHb. abstract (destruct (IHb x Hx Z d) as [y [Hy0 Hy1]]; split; auto; apply FinSubset_ball_cons, Hy0). Defined.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Hausdorff CoRN.logic.Classic CoRN.stdlib_omissions.List CoRN.metric2.Classification CoRN.metric2.Complete CoRN.metric2.Prelength