proposition: Lemma conv_fun_series_minus : fun_series_convergent _ _ Hab (fun n => f n{-}g n).
proof: Proof. elim convF; intros contF convF'. elim convG; intros contG convG'. assert (H := fun n : nat => Continuous_I_minus _ _ _ _ _ (contF n) (contG n)); exists H. cut (forall n : nat, Continuous_I Hab (fun_seq_part_sum f n{-}fun_seq_part_sum g n)); [ intro H0 | Contin ]. apply Cauchy_fun_seq_wd with (f := fun n : nat => fun_seq_part_sum f n{-}fun_seq_part_sum g n) (contf := H0). 2: eapply fun_Cauchy_prop_minus; auto; [ apply convF' | apply convG' ]. intros; apply eq_imp_Feq. Included. apply contin_imp_inc; Contin. intros; simpl in |- *. apply eq_symmetric_unfolded. apply eq_transitive_unfolded with (Sum0 n (fun i : nat => f i x (ProjIR1 Hx i)) [+] Sum0 n (fun i : nat => [--] (g i x (ProjIR2 Hx i)))). eapply eq_transitive_unfolded. 2: apply Sum0_plus_Sum0. apply Sum0_wd; intros; rational. unfold cg_minus in |- *. apply bin_op_wd_unfolded. algebra. eapply eq_transitive_unfolded. 2: apply inv_Sum0. apply Sum0_wd; algebra. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series