proposition: Lemma conv_imp_not_div : forall a, Cauchy_prop a -> Not (divergent_seq a).
proof: Proof. intros a Hconv. intro Hdiv. red in Hconv, Hdiv. elim Hdiv; clear Hdiv; intros e He He'. elim (Hconv _ (pos_div_three _ _ He)); clear Hconv; intros N HN. elim (He' N); clear He'; intros m Hm. elim Hm; clear Hm; intros n Hm'. elim Hm'; clear Hm'; intros Hm Hn. elim Hn; clear Hn; intros Hn Hmn. rewrite -> leEq_def in Hmn; apply Hmn. rstepr (e [/]ThreeNZ[+]e [/]ThreeNZ[+]e [/]ThreeNZ). apply leEq_less_trans with (AbsIR (a m[-]a N) [+]AbsIR (a N[-]a n)). eapply leEq_wdl. apply triangle_IR. apply AbsIR_wd; rational. astepl ([0][+]AbsIR (a m[-]a N) [+]AbsIR (a N[-]a n)). repeat apply plus_resp_less_leEq; try apply AbsSmall_imp_AbsIR; try exact (pos_div_three _ _ He). auto. apply AbsSmall_minus; auto. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)