proposition: Lemma Cauchy_fun_seq2_wd : Cauchy_fun_seq2 _ _ _ _ contf -> Cauchy_fun_seq2 _ _ _ _ contf0.
proof: Proof. intros H e H0. elim (H e H0); intros N HN. exists N; intros. eapply leEq_wdl. apply (HN m H1 x Hx). apply AbsIR_wd; rational. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval