proposition: Lemma b_seq_Cauchy : Cauchy_prop b_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 AbsIR_minus. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl (b_seq m). 2: astepl ( [--][--] (b_seq m)); astepr ( [--][--] (b_seq i)). 2: apply inv_resp_leEq; apply local_mon'_imp_mon' with (f := fun n : nat => [--] (b_seq n)); auto. 2: intro; apply inv_resp_leEq; apply b_seq_mon. eapply leEq_wdr. 2: apply a_seq_b_seq_dist. unfold cg_minus in |- *; apply plus_resp_leEq_lft. apply inv_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