proposition: Lemma IVT_gen (f : R -> R) (a b y : R) : Ranalysis1.continuity f -> Rmin (f a) (f b) <= y <= Rmax (f a) (f b) -> { x : R | Rmin a b <= x <= Rmax a b /\ f x = y }.
proof: Proof. case: (Req_EM_T a b) => [ <- {b} | Hab]. rewrite /Rmin /Rmax ; case: Rle_dec (Rle_refl a) (Rle_refl (f a)) ; case: Rle_dec => // _ _ _ _ Cf Hy. exists a ; split. split ; by apply Rle_refl. apply Rle_antisym ; by apply Hy. wlog: a b Hab / (a < b) => [Hw | {} Hab]. case: (Rle_lt_dec a b) => Hab'. case: (Rle_lt_or_eq_dec _ _ Hab') => {Hab'} // Hab'. by apply Hw. rewrite (Rmin_comm (f a)) (Rmin_comm a) (Rmax_comm (f a)) (Rmax_comm a) ; apply Hw => //. by apply Rlt_not_eq. rewrite /(Rmin a) /(Rmax a) ; case: Rle_dec (Rlt_le _ _ Hab) => // _ _. wlog: f y / (f a <= f b) => [Hw |]. case: (Rle_lt_dec (f a) (f b)) => Hf' Hf Hy. by apply Hw. case: (Hw (fun y => - f y) (- y)). by apply Ropp_le_contravar, Rlt_le. by apply Ranalysis1.continuity_opp. rewrite Rmin_opp_Rmax Rmax_opp_Rmin ; split ; apply Ropp_le_contravar, Hy. move => x [Hx Hfx]. exists x ; intuition. by rewrite -(Ropp_involutive y) -Hfx Ropp_involutive. rewrite /Rmin /Rmax ; case: Rle_dec => // _ _. wlog: y / (f a < y < f b) => [Hw Hf Hy | Hy Hf _]. case: Hy => Hay Hyb. case: (Rle_lt_or_eq_dec _ _ Hay) => {Hay} [Hay | <- ]. case: (Rle_lt_or_eq_dec _ _ Hyb) => {Hyb} [Hyb | -> ]. apply Hw ; intuition. exists b ; intuition. exists a ; intuition. case (IVT (fun x => f x - y) a b). apply Ranalysis1.continuity_minus. exact Hf. apply continuity_const. intros _ _ ; reflexivity. exact Hab. apply Rlt_minus_l ; rewrite Rplus_0_l ; apply Hy. apply Rlt_minus_r ; rewrite Rplus_0_l ; apply Hy. intros x [Hx Hfx]. apply Rminus_diag_uniq in Hfx. by exists x. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq