proposition: Lemma fun_Cauchy_prop_const_IR : forall H (contH:Continuous J H), Cauchy_fun_seq_IR J (fun n => H) (fun n => contH).
proof: Proof. intros. apply conv_Cauchy_fun_seq'_IR with H (contH). apply fun_Lim_seq_const_IR. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions