proposition: Lemma fun_conv_imp_seq_conv : conv_fun_seq' _ _ _ _ _ contf contF -> forall x, Compact Hab x -> forall Hxf HxF, Cauchy_Lim_prop2 (fun n => f n x (Hxf n)) (F x HxF).
proof: Proof. intros H x H0 Hxf HxF eps H1. elim (H eps H1). intros N HN. exists N; intros. apply AbsIR_imp_AbsSmall. eapply leEq_wdl. apply (HN m H2 x H0). apply AbsIR_wd; algebra. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval