proposition: Lemma FinEnum_prelength : PrelengthSpace FinEnum.
proof: Proof. intros a b e. revert a b. cut (forall d1 d2 : Qpos, proj1_sig e < proj1_sig (d1 + d2)%Qpos -> forall (a b:FinEnum), hemiMetricStrong X (proj1_sig e) (fun x : X => InFinEnumC x a) (fun x : X => InFinEnumC x b) -> exists2 c : FinEnum, ball (proj1_sig d1) a c & hemiMetric X (proj1_sig d2) (fun x : X => InFinEnumC x c) (fun x : X => InFinEnumC x b)). intros Z a b d1 d2 He H. destruct (HausdorffBallHausdorffBallStrong H) as [Hl Hr]. clear H. destruct (Z _ _ He _ _ Hl) as [c0 Hc0 Hc0c]. assert (He0: proj1_sig e < proj1_sig (d2 + d1)%Qpos). clear - He. abstract (simpl; rewrite -> Qplus_comm; assumption). destruct (Z _ _ He0 _ _ Hr) as [c1 Hc1 Hc1c]. clear Z Hl Hr. exists (c0 ++ c1). split. apply Qpos_nonneg. destruct Hc0 as [_ Hc0]. abstract ( destruct Hc0 as [Hc0a Hc0b]; destruct Hc1 as [Hc1a Hc1b]; split; intros x Hx; [destruct (Hc0a x Hx) as [ G | y [Hya Hyb]] using existsC_ind; [auto using existsC_stable | apply existsWeaken; exists y; unfold InFinEnumC; auto] |destruct (@FinSubset_ball_app_orC _ _ _ _ Hx) as [G | Hxl | Hxr] using orC_ind; [auto using existsC_stable |destruct (Hc0b x Hxl) as [ G | y [Hya Hyb]] using existsC_ind; [auto using existsC_stable | apply existsWeaken; exists y; auto] |destruct (Hc1c x Hxr) as [ G | y [Hya Hyb]] using existsC_ind; [auto using existsC_stable | apply existsWeaken; exists y; auto]]]). split. apply Qpos_nonneg. destruct Hc0 as [_ Hc0]. destruct Hc1 as [_ Hc1]. abstract ( destruct Hc0 as [Hc0a Hc0b]; destruct Hc1 as [Hc1a Hc1b]; split; intros x Hx; [destruct (@FinSubset_ball_app_orC _ _ _ _ Hx) as [G | Hxl | Hxr] using orC_ind; [auto using existsC_stable |destruct (Hc0c x Hxl) as [ G | y [Hya Hyb]] using existsC_ind; [auto using existsC_stable | apply existsWeaken; exists y; auto] |destruct (Hc1b x Hxr) as [ G | y [Hya Hyb]] using existsC_ind; [auto using existsC_stable | apply existsWeaken; exists y; auto]] |destruct (Hc1a x Hx) as [ G | y [Hya Hyb]] using existsC_ind; [auto using existsC_stable | apply existsWeaken; exists y; unfold InFinEnumC; auto]]). intros d1 d2 He a b H. induction a. exists nil. apply ball_refl. apply Qpos_nonneg. intros x Hx; exfalso; exact (FinSubset_ball_nil Hx). destruct IHa as [c1 Hc1a Hc1b]. abstract (intros x Hx d; apply (H x); apply FinSubset_ball_cons, Hx). destruct (Qpos_sub _ _ He) as [g Hg]. pose (exist (Qlt 0) (1#2) eq_refl) as half. destruct (fun z => H a z (half*g)%Qpos) as [b0 Hb0]. abstract (intro abs; contradict abs; exists a; split; [left; reflexivity | reflexivity]). clear H. destruct (@preLengthX a b0 (e + half * g)%Qpos d1 d2) as [c Hc0 Hc1]. abstract ( clear - Hg; unfold QposEq in Hg; rewrite -> Hg; simpl; rewrite -> Qlt_minus_iff; ring_simplify; apply (Qpos_ispos ((1#2)*g))). abstract (clear - Hb0; destruct Hb0; auto). exists (c :: c1). - split. apply Qpos_nonneg. split; intros x Hx. + apply FinSubset_ball_orC in Hx. destruct Hx as [ G | Hx | Hx ] using orC_ind. auto using existsC_stable. apply existsWeaken. exists c. split. intro abs; contradict abs; exists c; split; [left; reflexivity | reflexivity]. rewrite Hx. assumption. destruct Hc1a as [_ Hc1a]. destruct Hc1a as [Hc1a _]. destruct (Hc1a x Hx) as [ G | y [Hy0 Hy1]] using existsC_ind; [auto using existsC_stable|]. apply existsWeaken; exists y; split; auto. apply FinSubset_ball_cons. exact Hy0. + apply FinSubset_ball_orC in Hx. destruct Hx as [ G | Hx | Hx ] using orC_ind. auto using existsC_stable. apply existsWeaken; exists a; split. intro abs; contradict abs; exists a; split; [left; reflexivity | reflexivity]. apply (ball_wd _ eq_refl _ _ Hx _ _ (reflexivity _)); auto with *. destruct Hc1a as [_ Hc1a]. destruct Hc1a as [_ Hc1a]; destruct (Hc1a x Hx) as [ G | y [Hy0 Hy1]] using existsC_ind; [auto using existsC_stable|]; apply existsWeaken; exists y; split; auto. apply (@FinSubset_ball_cons y). exact Hy0. - destruct Hb0 as [Hb0a Hb0b]; intros x Hx. apply FinSubset_ball_orC in Hx. destruct Hx as [ G | Hx | Hx ] using orC_ind. auto using existsC_stable. apply existsWeaken; exists b0; split; auto. apply (ball_wd _ eq_refl _ _ Hx _ _ (reflexivity _)); auto. apply Hc1b; 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