proposition: Lemma Cauchy_fun_seq_wd : (forall n, Feq I (f n) (g n)) -> Cauchy_fun_seq _ _ _ _ contf -> Cauchy_fun_seq _ _ _ _ contg.
proof: Proof. intros H H0 e H1. elim (H0 e H1); clear H0; intros N HN. exists N; intros. eapply leEq_wdl. apply (HN m n H0 H2 x Hx). elim (H n); intros. inversion_clear b0. elim (H m); intros. inversion_clear b0. apply AbsIR_wd; algebra. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval