proposition: Lemma IVT_interval : forall (f : R -> R) (x y : R) l, continuity_interval x y f -> x <= y -> interval (f x) (f y) l -> {z : R | interval x y z /\ f z = l}.
proof: Proof. intros f x y l Hf xley [fxlel llefy] ; destruct (Rle_lt_or_eq_dec _ _ xley) as [xlty | xeqy]. destruct (Rle_lt_or_eq_dec _ _ fxlel) as [fxltl | fxeql]. destruct (Rle_lt_or_eq_dec _ _ llefy) as [lltfy | leqfy]. destruct (IVT_open_interval _ _ _ l Hf xlty) as [z [z_in Hz]]. split ; assumption. exists z ; split ; [apply open_interval_interval |] ; assumption. exists y ; split ; [apply interval_r |] ; auto. exists x ; split ; [apply interval_l |] ; auto. exists y ; subst ; split ; [apply interval_r | apply Rle_antisym] ; auto. Qed.
imports: Rbase Rsequence Ranalysis Rfunctions Rseries_def Lra RiemannInt SeqProp MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity