proposition: Lemma conv_fun_seq_wd : forall a b Hab f contf contf0, conv_fun_seq a b Hab f contf -> conv_fun_seq a b Hab f contf0.
proof: Proof. intros a b Hab f contf contf0 H. elim H; intros f' Hf'. exists f'. elim Hf'; intros contf' H0. exists contf'. eapply conv_fun_seq'_wd. apply H0. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval