proposition: Lemma comparison : forall y, convergent y -> (forall n, AbsIR (x n) [<=] y n) -> convergent x.
proof: Proof. intros y H H0. apply str_comparison with y. assumption. exists 0; intros; apply H0. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)