proposition: Lemma leR_bigmaxR : forall m, m \in s -> F m <= \rmax_(m <- s) (F m).
proof: Proof. elim: s => // hd tl IH m; rewrite in_cons; case/orP. - move/eqP => ->; rewrite big_cons; exact/leR_maxl. - move/IH => H; rewrite big_cons; exact/(leR_trans H)/leR_maxr. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)