proposition: Lemma conv_Cauchy_fun_seq : conv_fun_seq _ _ _ _ contf -> Cauchy_fun_seq _ _ _ _ contf.
proof: Proof. intro H. elim H; intros ff Hff. inversion_clear Hff. apply conv_Cauchy_fun_seq' with (PartInt ff) x. unfold I in |- *; eapply conv_fun_seq'_wd. apply X. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval