proposition: Lemma a_seq_Cauchy : Cauchy_prop a_seq.
proof: Proof. intros e H. elim (intervals_small' a b e H); intros i Hi. exists i; intros. apply AbsIR_imp_AbsSmall. eapply leEq_transitive. 2: apply Hi. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl (a_seq i). 2: apply local_mon'_imp_mon'; auto; exact a_seq_mon. eapply leEq_wdr. 2: apply a_seq_b_seq_dist. apply minus_resp_leEq. apply less_leEq; apply a_b'. exact a_seq_mon. exact b_seq_mon. exact a_seq_less_b_seq. Qed.
imports: CoRN.ftc.Continuity