proposition: Lemma FinSubset_ball_map : forall (e d:Qpos) a (b:FinEnum X), (QposInf_le d (mu f e)) -> FinSubset_ball (proj1_sig d) a b -> FinSubset_ball (proj1_sig e) (f a) (FinEnum_map z f b).
proof: Proof. intros e d a b Hd Hab. induction b. exfalso; exact (FinSubset_ball_nil Hab). apply FinSubset_ball_orC in Hab. destruct Hab as [G | Hab | Hab] using orC_ind. intro abs; contradict G; intro G; contradiction. intro abs; contradict abs. exists (f a0). split. left. reflexivity. apply uc_prf. eapply ball_ex_weak_le. apply Hd. assumption. apply FinSubset_ball_cons. apply IHb. auto. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround CoRN.metric2.Prelength