proposition: Lemma divergent_imp_not_convergent : divergent -> Not convergent.
proof: Proof. intro H. intro H0. red in H, H0. generalize H0; apply div_imp_not_conv. assumption. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)