proposition: Lemma HemiMetricStrongAlmostDecidableBody : forall (e d:Q) a (b : FinEnum), e < d -> {hemiMetric X d (fun x => msp_eq x a) (fun x => InFinEnumC x b)} + {~hemiMetric X e (fun x => msp_eq x a) (fun x => InFinEnumC x b)}.
proof: Proof. intros e d a b. induction b. - intros Hed. right. abstract (intros H; apply (H a); try reflexivity; intros x [Hx0 Hx1]; exact (FinSubset_ball_nil Hx0)). - intros Hed. destruct (IHb Hed) as [H|H]. left. abstract (intros x Hx; destruct (H x Hx) as [HG | z [Hz0 Hz1]] using existsC_ind; [apply existsC_stable; auto|]; apply existsWeaken; exists z; split; try assumption; apply FinSubset_ball_cons, Hz0). destruct (@almostDecideX _ _ a a0 Hed). + left. intros x Hx; apply existsWeaken; exists a0. split. auto using InFinEnumC_weaken with *. apply (ball_wd _ eq_refl _ _ Hx _ _ (reflexivity _)). auto using InFinEnumC_weaken with *. + right. intros H0; assert (Haa:msp_eq a a) by reflexivity; destruct (H0 a Haa) as [HG | z [Hz0 Hz1]] using existsC_ind; [tauto|]. apply FinSubset_ball_orC in Hz0. destruct Hz0 as [HG | Hz2 | Hz2] using orC_ind. tauto. apply (ball_wd _ eq_refl _ _ (reflexivity _) _ _ Hz2) in Hz1. contradiction. apply H; intros x Hx; apply existsWeaken; exists z. split. exact Hz2. apply (ball_wd _ eq_refl _ _ Hx _ _ (reflexivity _)). auto. 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