proposition: Lemma Cauchy_fun_real : Cauchy_fun_seq -> forall x Hx, Cauchy_prop (fun n => Part _ _ (incf n x Hx)).
proof: Proof. intros H x Hx. red in |- *; red in H. intros e He. elim (H _ He); clear H; intros N HN. exists N. intros. apply AbsIR_imp_AbsSmall. apply HN. assumption. apply le_n. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval