proposition: Lemma Cnested_intervals_zero : {z : IR | a 0 [<=] z /\ z [<=] b 0 /\ f z [=] [0]}.
proof: Proof. elim Cnested_intervals_limit. intro z. intros H0 H1. exists z. split. auto. split. auto. apply not_ap_imp_eq. unfold Not in |- *. intros H2. elim (ap_imp_less _ _ _ H2); intros H3. elim (f_contin_neg z H3). intro eps. intros H5 H6. elim (b_a eps). intro i. intros H7. cut (b i [<=] z[+]eps). intro. cut (z [<=] b i[+]eps). intro. pose (c:= f_b i). rewrite -> leEq_def in c. apply c. apply H6. auto. auto. apply leEq_transitive with (b i). auto. astepl (b i[+][0]). apply plus_resp_leEq_lft. apply less_leEq. auto. apply leEq_transitive with (a i[+]eps). auto. apply plus_resp_leEq. auto. auto. elim (f_contin_pos z H3). intro eps. intros H5 H6. elim (b_a eps). intro i. intros H7. cut (a i [<=] z[+]eps). intro. cut (z [<=] a i[+]eps). intro. pose (c:= f_a i). rewrite -> leEq_def in c; apply c. apply H6. auto. auto. apply leEq_transitive with (b i). auto. auto. apply leEq_transitive with z. auto. astepl (z[+][0]). apply less_leEq. apply plus_resp_less_lft. auto. auto. Qed.
imports: CoRN.reals.CPoly_Contin