proposition: Lemma Civt_op : {z : IR | a [<=] z /\ z [<=] b /\ f z [=] [0]}.
proof: Proof. cut (forall i : nat, a_ i [<=] a_ (S i)). intro H. cut (forall i : nat, b_ (S i) [<=] b_ i). intro H0. cut (forall i : nat, a_ i [<] b_ i). intro H1. cut (forall i : nat, f (a_ i) [<=] [0]). intro H2. cut (forall i : nat, [0] [<=] f (b_ i)). intro H3. elim (Cnested_intervals_zero a_ b_ H H0 H1 intervals_small f f_contin H2 H3). intro z. intro H4. exists z. exact H4. intros. exact (interval_f_rht _ (interval_sequence i)). intros. exact (interval_f_lft _ (interval_sequence i)). intros. exact (interval_lft_rht _ (interval_sequence i)). intros. elim (bisect_prop f f_apzero_interval (interval_sequence i)). intros H0 H1. elim H1. intros H2 H3. unfold b_ in |- *. simpl in |- *. assumption. intros. elim (bisect_prop f f_apzero_interval (interval_sequence i)). intros H H0. elim H0. intros H1 H2. unfold a_ in |- *. simpl in |- *. auto. Qed.
imports: CoRN.reals.CPoly_Contin