proposition: Lemma bisect_prop : forall I : bisect_interval, interval_rht (bisect I) [-]interval_lft (bisect I) [<=] Small[*] (interval_rht I[-]interval_lft I) /\ interval_lft I [<=] interval_lft (bisect I) /\ interval_rht (bisect I) [<=] interval_rht I.
proof: Proof. intros. unfold bisect in |- *. apply proj2_sigT. Qed.
imports: CoRN.reals.CPoly_Contin