proposition: Lemma intervals_smaller : forall i, b_ i[-]a_ i [<=] Small[^]i[*] (b[-]a).
proof: Proof. intros. induction i as [| i Hreci]; intros. unfold a_ in |- *. unfold b_ in |- *. simpl in |- *. rstepr (b[-]a). apply leEq_reflexive. apply leEq_transitive with (Small[*] (b_ i[-]a_ i)). elim (bisect_prop f f_apzero_interval (interval_sequence i)). intros H H0. elim H0; intros H1 H2. auto. simpl in |- *. replace (nexp _ i Small) with (Small[^]i). 2: auto. rstepr (Small[*] (Small[^]i[*] (b[-]a))). apply mult_resp_leEq_lft. auto. apply less_leEq. unfold Small in |- *. apply div_resp_pos. apply pos_three. apply pos_two. Qed.
imports: CoRN.reals.CPoly_Contin