proposition: Lemma Cbisect' : {a' : IR | {b' : IR | a' [<] b' | a [<=] a' /\ b' [<=] b /\ b'[-]a' [<=] Small[*] (b[-]a) /\ f a' [<=] [0] /\ [0] [<=] f b'}}.
proof: Proof. elim (f_apzero_interval lft rht lft_rht). intro c. intro H. elim H. intros H0 H2 H3. cut ({f c [<=] [0]} + {[0] [<=] f c}). intro H4; inversion_clear H4. exists c. exists b. apply leEq_less_trans with rht. auto. apply rht_b. split. apply leEq_transitive with lft. apply less_leEq. apply a_lft. auto. split. apply leEq_reflexive. split. astepr (b[-]lft). apply minus_resp_leEq_rht. auto. split. auto. auto. exists a. exists c. apply less_leEq_trans with lft. apply a_lft. auto. split. apply leEq_reflexive. split. apply less_leEq. apply leEq_less_trans with rht. auto. apply rht_b. split. astepr (rht[-]a). apply minus_resp_leEq. auto. split. auto. auto. elim (ap_imp_less _ _ _ H3); intros. left. apply less_leEq. auto. right. apply less_leEq. auto. Qed.
imports: CoRN.reals.CPoly_Contin