proposition: Lemma fun_Cauchy_prop_inv : forall H, Cauchy_fun_seq a b Hab (fun n => {--} (f n)) H.
proof: Proof. intro. cut (Continuous_I Hab {--} (Cauchy_fun_seq_Lim _ _ _ _ _ Hf)); [ intro H0 | Contin ]. apply conv_Cauchy_fun_seq' with ( {--} (Cauchy_fun_seq_Lim _ _ _ _ _ Hf)) H0. apply fun_Lim_seq_inv. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval