proposition: Lemma Cauchy_conv_fun_seq_IR : Cauchy_fun_seq_IR _ _ contf -> conv_fun_seq_IR _ _ contf.
proof: Proof. intros H a b Hab Hinc. eapply Cauchy_conv_fun_seq. apply (H a b Hab Hinc). Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions