proposition: Lemma intervals_small' : forall eps, [0] [<] eps -> {i : nat | Small[^]i[*] (b[-]a) [<=] eps}.
proof: Proof. intros. cut (eps [#] [0]). intro H0. elim (Archimedes (b[-]a[/] eps[//]H0)). intro i. intros H1. exists i. astepr (eps[*][1]). apply shift_leEq_mult' with H0. auto. apply leEq_transitive with (Small[^]i[*]nring i). astepl (Small[^]i[*] (b[-]a[/] eps[//]H0)). apply mult_resp_leEq_lft. auto. apply nexp_resp_nonneg. apply less_leEq. astepl (ZeroR [/]ThreeNZ). unfold Small in |- *. apply div_resp_less_rht. apply pos_two. apply pos_three. apply intervals_small''. apply Greater_imp_ap. auto. Qed.
imports: CoRN.reals.CPoly_Contin