proposition: Lemma conv_fun_seq'_wd : conv_fun_seq' _ _ _ _ _ contf contF -> conv_fun_seq' _ _ _ _ _ contf0 contF0.
proof: Proof. intros H e H0. elim (H e H0); intros N HN. exists N; intros. eapply leEq_wdl. apply (HN n H1 x Hx). apply AbsIR_wd; rational. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval