proposition: Lemma FinEnum_map_Cunit : forall X (s1 s2:FinEnum X) (e:Qpos), ball (proj1_sig e) s1 s2 <-> ball (proj1_sig e) (map Cunit s1:FinEnum (Complete X)) (map Cunit s2).
proof: Proof. intros X s1 s2 e. split. - intros H. exact (@FinEnum_map_uc (1 # 1) _ _ Cunit e s1 s2 H). - revert s1 s2. cut (forall (s1 s2 : FinEnum X) , hemiMetric (Complete X) (proj1_sig e) (fun a => InFinEnumC a (map Cunit s1:FinEnum (Complete X))) (fun a => InFinEnumC a (map Cunit s2)) -> hemiMetric X (proj1_sig e) (fun a => InFinEnumC a s1) (fun a => InFinEnumC a s2)). { intros Z s1 s2. intros [epos [H0 H1]]. split. exact epos. split; apply Z; assumption. } intros s1 s2 H a Ha. induction s1. exfalso; exact (FinSubset_ball_nil Ha). apply FinSubset_ball_orC in Ha. destruct Ha as [G | Ha | Ha] using orC_ind. auto using existsC_stable. clear IHs1. assert (Ha0:InFinEnumC (Cunit a0) (map Cunit (a0::s1))). intro abs; contradict abs. exists (Cunit a0). split. left; reflexivity. reflexivity. destruct (H _ Ha0) as [G | y [Hy0 Hy1]] using existsC_ind. auto using existsC_stable. clear - Ha Hy0 Hy1. induction s2. exfalso; exact (FinSubset_ball_nil Hy0). apply FinSubset_ball_orC in Hy0. destruct Hy0 as [G | Hy0 | Hy0] using orC_ind. auto using existsC_stable. apply existsWeaken. exists a1. split. intro abs; contradict abs. exists a1. split. left; reflexivity. reflexivity. rewrite Ha. rewrite <- ball_Cunit. rewrite <- Hy0. assumption. destruct (IHs2 Hy0) as [G | z [Hz0 Hz1]] using existsC_ind. auto using existsC_stable. apply existsWeaken. exists z. split; auto. apply FinSubset_ball_cons. exact Hz0. apply IHs1; auto. intros b Hb. apply H. apply FinSubset_ball_cons. exact Hb. 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