proposition: Lemma ex_Im_fct (f : R -> R) (a b : R) : a <> b -> exists x, (fun y => exists x, y = f x /\ Rmin a b < x < Rmax a b) x.
proof: Proof. exists (f ((a+b)/2)) ; exists ((a+b)/2) ; split. by []. rewrite /Rmin /Rmax. case Rle_dec ; lra. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy