proposition: Lemma Cauchy_conv_fun_seq' : forall H contf', conv_fun_seq' _ _ _ _ (Cauchy_fun_seq_Lim _ _ _ f contf H) contf contf'.
proof: Proof. intros H contf' e H0. elim (H e H0). intros N HN. exists N. intros. set (incf := fun n : nat => contin_imp_inc _ _ _ _ (contf n)) in *. set (incf' := contin_imp_inc _ _ _ _ contf') in *. apply leEq_wdl with (AbsIR (Lim (Cauchy_const (f n x (incf n x Hx))) [-] Part (Cauchy_fun_seq_Lim _ _ _ _ _ H) x (incf' x Hx))). 2: apply AbsIR_wd; apply cg_minus_wd. 2: apply eq_symmetric_unfolded; apply Lim_const. 2: algebra. simpl in |- *. apply leEq_wdl with (AbsIR (Lim (Build_CauchySeq IR _ (Cauchy_minus (Cauchy_const (Part _ _ (incf n x Hx))) (Build_CauchySeq _ _ (Cauchy_fun_real _ _ _ _ _ H x (incf' x Hx))))))). 2: apply AbsIR_wd; apply Lim_minus. eapply leEq_wdl. 2: apply Lim_abs. simpl in |- *. apply str_seq_leEq_so_Lim_leEq. exists N; intros. simpl in |- *. eapply leEq_wdl. apply (HN n i H1 H2 x Hx). apply AbsIR_wd; rational. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval