proposition: Lemma Cauchy_conv_fun_seq'_IR : forall H contf', conv_fun_seq'_IR _ _ (Cauchy_fun_seq_Lim_IR _ _ contf H) contf contf'.
proof: Proof. intros. red in |- *; intros. eapply conv_fun_seq'_wdr. apply Feq_symmetric. apply (Cauchy_fun_seq_Lim_char J f contf H a b Hab Hinc). apply Cauchy_conv_fun_seq' with (H := H a b Hab Hinc) (contf' := Cauchy_cont_Lim _ _ _ _ _ (H a b Hab Hinc)). Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions