proposition: Lemma Inf_fct_le (f : R -> R) (a b : R) (x : R) : (Rmin a b < x < Rmax a b) -> Rbar_le (Inf_fct f a b) (Finite (f x)).
proof: Proof. move => Hx ; rewrite /Inf_fct. case: Req_EM_T => Hab. move: (Rlt_trans _ _ _ (proj1 Hx) (proj2 Hx)) => {Hx} ; rewrite /Rmin /Rmax ; case: Rle_dec (Req_le _ _ Hab) => //= _ _ Hx. contradict Hx ; by apply Rle_not_lt, Req_le. rewrite /Glb_Rbar ; case: ex_glb_Rbar => l lub ; apply lub ; exists x ; split ; by []. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy