proposition: Lemma Cauchy_cont_Lim_IR : forall H, Continuous J (Cauchy_fun_seq_Lim_IR _ _ contf H).
proof: Proof. intros. split; Included. intros a b Hab H0; eapply Continuous_I_wd. apply Feq_symmetric. apply (Cauchy_fun_seq_Lim_char J f contf H a b Hab H0). Contin. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions