proposition: Lemma intervals_cauchy : Cauchy_prop a.
proof: Proof. unfold Cauchy_prop in |- *. unfold AbsSmall in |- *. intro eps. intros H. elim (b_a eps H). intro n. intros. exists n. intro i. intros. split; apply less_leEq. apply less_leEq_trans with ZeroR. astepr ( [--]ZeroR). apply inv_resp_less. auto. astepl (a n[-]a n). apply minus_resp_leEq. apply a_mon'. auto. apply shift_minus_less'. apply less_leEq_trans with (b n). apply a_b'. auto. Qed.
imports: CoRN.reals.CPoly_Contin