proposition: Lemma IVT_open_interval_prelim : forall (f : R -> R) (x y : R), continuity_interval x y f -> x < y -> open_interval (f x) (f y) 0 -> {z : R | open_interval x y z /\ f z = 0}.
proof: Proof. intros f x y Hf xlty O_in ; assert (xley := Rlt_le _ _ xlty) ; pose (P := fun z => cond_positivity (f z)) ; pose (Zn := dicho_up x y P) ; pose (Zn' := dicho_lb x y P) ; assert (Hcv := dicho_diff_cv _ _ P xley) ; destruct (dicho_up_cv x y P xley) as [z Hz] ; exists z. assert (Hz' : Rseq_cv Zn' z). destruct (dicho_lb_cv x y P xley) as [z' Hz'] ; rewrite <- (cv_dicho _ _ _ _ _ xley Hz' Hz) ; assumption. assert (fz_eq : f z = 0). apply Rle_antisym. apply Rseq_negative_limit with (fun n => f (Zn' n)). intro n ; left ; rewrite <- cond_positivity_car' ; fold (P (Zn' n)) ; apply dicho_lb_car ; unfold P ; rewrite cond_positivity_car' ; apply O_in. eapply Rseq_cv_continuity_interval_compat ; [eapply dicho_interval_compat | intro ; apply dicho_steps_interval_compat | |] ; eassumption. apply Rseq_positive_limit with (fun n => f (Zn n)). intro n ; rewrite <- cond_positivity_car ; fold (P (Zn n)) ; apply dicho_up_car ; unfold P ; rewrite cond_positivity_car ; left ; apply O_in. eapply Rseq_cv_continuity_interval_compat ; [eapply dicho_interval_compat | intro ; apply dicho_steps_interval_compat | |] ; eassumption. split ; [apply interval_open_interval | assumption]. eapply dicho_interval_compat ; eassumption. intro Hfalse ; rewrite Hfalse in O_in ; apply (Rlt_irrefl 0) ; apply Rle_lt_trans with (f z) ; [right ; symmetry ; apply fz_eq | apply O_in]. intro Hfalse ; rewrite Hfalse in O_in ; apply (Rlt_irrefl 0) ; apply Rlt_le_trans with (f z) ; [apply O_in | right ; apply fz_eq]. Qed.
imports: Rbase Rsequence Ranalysis Rfunctions Rseries_def Lra RiemannInt SeqProp MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity