proposition: Lemma continuous_ab_maj_consistent : forall (f : R -> R) (a b : R), a <= b -> (forall c : R, a <= c <= b -> continuous f c) -> exists Mx : R, (forall c : R, a <= c <= b -> f c <= f Mx) /\ a <= Mx <= b.
proof: Proof. move => f a b Hab Hc. apply: continuity_ab_maj => // . by move => c Hc1; apply continuity_pt_filterlim; exact: Hc. 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