proposition: Lemma Cauchy_fun_seq2_seq : Cauchy_fun_seq2 -> Cauchy_fun_seq.
proof: Proof. intro H. red in |- *; red in H. intros e H0. elim (H _ (pos_div_two _ _ H0)); intros N HN; exists N; intros. apply leEq_wdl with (AbsIR (Part _ _ (incf m x Hx) [-]Part _ _ (incf N x Hx) [-] (Part _ _ (incf n x Hx) [-]Part _ _ (incf N x Hx)))). 2: apply AbsIR_wd; rational. eapply leEq_transitive. apply triangle_IR_minus. rstepr (e [/]TwoNZ[+]e [/]TwoNZ). apply plus_resp_leEq_both; apply HN; auto with arith. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval