proposition: Lemma Cauchy_fun_seq_wd_IR : (forall n, Feq J (f n) (g n)) -> Cauchy_fun_seq_IR _ _ contf -> Cauchy_fun_seq_IR _ _ contg.
proof: Proof. intros H H0 a b Hab Hinc. eapply Cauchy_fun_seq_wd with (f := f). 2: apply (H0 a b Hab Hinc). intro; apply included_Feq with J; auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions