proposition: Lemma HemiMetricStrongAlmostDecidable : forall (e d:Q) (a b : FinEnum), e < d -> {hemiMetric X d (fun x => InFinEnumC x a) (fun x => InFinEnumC x b)} + {~hemiMetric X e (fun x => InFinEnumC x a) (fun x => InFinEnumC x b)}.
proof: Proof. induction a. intros a _. left. intros x Hx _. exact (FinSubset_ball_nil Hx). intros b Hed. destruct (IHa b Hed) as [I|I]. destruct (@HemiMetricStrongAlmostDecidableBody _ _ a b Hed) as [J|J]. left. abstract ( intros x Hx; apply FinSubset_ball_orC in Hx; destruct Hx as [HG | ? | ?] using orC_ind; [auto using existsC_stable |apply J; assumption |apply I; assumption]). right. abstract (intros H; apply J; intros x Hx; apply H; intro abs; contradict abs; exists a; split; [left; reflexivity | apply Hx]). right. abstract (intros H; apply I; intros x Hx; apply H; apply FinSubset_ball_cons, Hx). 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