proposition: Lemma convergent_imp_inc : fun_series_convergent_IR J f -> forall n, included J (Dom (f n)).
proof: Proof. intros H n. apply included_imp_inc. intros a b Hab H0. red in H. elim (H _ _ _ H0); intros. apply contin_imp_inc; auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions