proposition: Lemma Cbisect_exists : forall I : bisect_interval, {I' : bisect_interval | interval_rht I'[-]interval_lft I' [<=] Small[*] (interval_rht I[-]interval_lft I) /\ interval_lft I [<=] interval_lft I' /\ interval_rht I' [<=] interval_rht I}.
proof: Proof. intros. elim (Cbisect' f C_f_apzero_interval _ _ (interval_lft_rht I) ( interval_f_lft I) (interval_f_rht I)). intro lft. intro H. elim H. intro rht. intros H1 H2. elim H2. intros H3 H4. elim H4. intros H5 H6. elim H6. intros H7 H8. elim H8. intros H9 H10. exists (Build_bisect_interval lft rht H1 H9 H10). simpl in |- *. unfold Small in |- *. split. auto. split. auto. auto. Qed.
imports: CoRN.reals.CPoly_Contin