proposition: Lemma Cauchy_conv_fun_seq : Cauchy_fun_seq _ _ _ _ contf -> conv_fun_seq _ _ _ _ contf.
proof: Proof. intro H. cut (Continuous_I Hab (Cauchy_fun_seq_Lim _ _ _ _ _ H)). intro H0. exists (IntPartIR (contin_imp_inc _ _ _ _ H0)). cut (Continuous_I Hab (PartInt (IntPartIR (contin_imp_inc _ _ _ _ H0)))). 2: eapply Continuous_I_wd. 3: apply Cauchy_cont_Lim with (H := H). 2: FEQ. 2: simpl in |- *; apply Lim_wd'; intros; algebra. intro H2; exists H2. intros e H1. elim (Cauchy_conv_fun_seq' H H0 e H1); intros N HN. exists N; intros. eapply leEq_wdl. apply (HN n H3 x Hx). apply AbsIR_wd; apply cg_minus_wd. algebra. simpl in |- *; apply Lim_wd'; intros; simpl in |- *; rational. simpl in |- *; algebra. simpl in |- *; apply Cauchy_cont_Lim. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval