proposition: Lemma Cauchy_fun_seq_seq' : Cauchy_fun_seq -> Cauchy_fun_seq'.
proof: Proof. intro H. red in |- *; red in H. intro. exact (H (one_div_succ k) (one_div_succ_pos _ k)). Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval