proposition: Lemma conv_series_minus : convergent (fun n => x n[-]y n).
proof: Proof. red in |- *. red in convX, convY. eapply Cauchy_prop_wd. apply Cauchy_minus with (seq1 := Build_CauchySeq _ _ convX) (seq2 := Build_CauchySeq _ _ convY). simpl in |- *. unfold seq_part_sum in |- *. intro. apply eq_symmetric_unfolded; unfold cg_minus in |- *. eapply eq_transitive_unfolded. apply Sum0_plus_Sum0 with (g := fun n : nat => [--] (y n)). apply bin_op_wd_unfolded. algebra. apply inv_Sum0. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)