proposition: Lemma Sup_fct_maj (f : R -> R) (a b : R) (M : R) : (forall x, Rmin a b < x < Rmax a b -> f x <= M) -> is_finite (Sup_fct f a b).
proof: Proof. rewrite /Sup_fct ; case: Req_EM_T => Hab Hf. by []. rewrite /Lub_Rbar ; case: ex_lub_Rbar ; case => [l | | ] [lub ub] /=. by []. case: (ub (Finite M)) => //. move => _ [x [-> Hx]]. by apply Hf. case: (lub (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