proposition: Lemma conv_Cauchy_fun_seq' : conv_fun_seq' -> Cauchy_fun_seq.
proof: Proof. intro H. red in |- *; red in H. intros e He. elim (H _ (pos_div_two _ _ He)). intros N HN. exists N; intros. apply leEq_wdl with (AbsIR (f m x (incf m x Hx) [-]F x (incF x Hx) [+] (F x (incF x Hx) [-]f n x (incf n x Hx)))). 2: apply AbsIR_wd; rational. eapply leEq_transitive. apply triangle_IR. rstepr (e [/]TwoNZ[+]e [/]TwoNZ). apply plus_resp_leEq_both. apply HN; assumption. eapply leEq_wdl. 2: apply AbsIR_minus. apply HN; assumption. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval