proposition: Lemma div_imp_not_conv : forall a, divergent_seq a -> Not (Cauchy_prop a).
proof: Proof. intros a H. red in |- *; intro H0. generalize H; generalize H0. apply conv_imp_not_div. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)