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