proposition: Lemma fun_Lim_seq_plus'_IR : forall H H', conv_fun_seq'_IR J (fun n => f n{+}g n) (F{+}G) H H'.
proof: Proof. intros. red in |- *; intros. eapply fun_Lim_seq_plus'. apply (convF a b Hab Hinc). apply (convG a b Hab Hinc). Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions