proposition: Lemma Cauchy_fun_seq1_seq' : Cauchy_fun_seq1 -> Cauchy_fun_seq'.
proof: Proof. intro H. red in |- *; red in H. intro. elim (H k); clear H; intros N HN. exists N; intros. eapply leEq_transitive. 2: apply HN with (m := m) (n := n); assumption. cut (Dom (f m{-}f n) x). intro H1. apply leEq_wdl with (AbsIR (Part _ _ H1)). apply norm_bnd_AbsIR; assumption. apply AbsIR_wd; simpl in |- *; rational. split; simpl in |- *; apply incf; assumption. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval