proposition: Lemma IVT_gen_consistent (f : R -> R) (a b y : R) : (forall x, continuous f x) -> 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. move => Hf. apply: IVT_gen. move => x. apply continuity_pt_filterlim. exact: Hf. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(eqtype seq) Markov Rcomplements Rbar Lub Lim_seq Derive SF_seq Continuity Hierarchy Seq_fct RInt PSeries