proposition: Lemma fun_Lim_seq_const_IR : forall H contH contH', conv_fun_seq'_IR J (fun n => H) H contH contH'.
proof: Proof. exists 0; intros. eapply leEq_wdl. 2: eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply AbsIRz_isz. apply less_leEq; assumption. apply AbsIR_wd; rational. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions