proposition: Lemma IVT_open_interval : forall (f : R -> R) (x y : R) l, continuity_interval x y f -> x < y -> open_interval (f x) (f y) l -> { z : R | open_interval x y z /\ f z = l }.
proof: Proof. intros f x y l Hf Hxy Hl ; destruct IVT_open_interval_prelim with (f - (fun _ => l))%F x y as [z [z_in Hz]]. apply continuity_in_minus, continuity_in_const ; assumption. assumption. clear - Hl; destruct Hl ; split ; unfold minus_fct ; lra. exists z ; split ; [assumption |]. clear - Hz ; unfold minus_fct in * ; intuition. Qed.
imports: Rbase Rsequence Ranalysis Rfunctions Rseries_def Lra RiemannInt SeqProp MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity