proposition: Lemma conv_fun_const_series : forall x, convergent x -> fun_series_convergent _ _ Hab (fun n => [-C-] (x n)).
proof: Proof. intros x H. exists (fun n : nat => Continuous_I_const _ _ Hab (x n)). apply Cauchy_fun_seq2_seq. red in |- *; intros e He. elim (H e He); intros N HN. exists N; intros. simpl in |- *. apply AbsSmall_imp_AbsIR. apply AbsSmall_wdr_unfolded with (seq_part_sum x m[-]seq_part_sum x N). apply HN; assumption. unfold seq_part_sum in |- *; simpl in |- *. apply cg_minus_wd; apply Sum0_wd; algebra. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series