proposition: Lemma abs_imp_conv : abs_convergent x -> convergent x.
proof: Proof. intros H. apply Convergence_Criteria.comparison with (fun n : nat => AbsIR (x n)). apply H. intro; apply leEq_reflexive. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)