fact: Fixpoint interval_sequence (n : nat) : bisect_interval f := match n with | O => Build_bisect_interval f a b a_b f_a f_b | S m => bisect f f_apzero_interval (interval_sequence m) end.
imports: CoRN.reals.CPoly_Contin