proposition: Lemma intervals_small : forall eps, [0] [<] eps -> {i : nat | b_ i [<=] a_ i[+]eps}.
proof: Proof. intros eps H. elim (intervals_small' eps H). intro i. intros. exists i. apply shift_leEq_plus'. apply leEq_transitive with (Small[^]i[*] (b[-]a)). apply intervals_smaller. auto. Qed.
imports: CoRN.reals.CPoly_Contin