proposition: Lemma conv_fun_seq'_wdl : (forall n, Feq I (f n) (g n)) -> conv_fun_seq' _ _ _ _ _ contf contF -> conv_fun_seq' _ _ _ _ _ contg contF0.
proof: Proof. intros H H0 e H1. elim (H0 e H1); intros N HN. exists N; intros. eapply leEq_wdl. apply (HN n H2 x Hx). apply AbsIR_wd; apply cg_minus_wd. elim (H n); intros Haux inc. inversion_clear inc. auto. algebra. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval