proposition: Lemma bigmaxR_ge0 : (forall r, r \in s -> 0 <= F r) -> 0 <= \rmax_(m <- s) (F m).
proof: Proof. case: s => [_ | hd tl Hr]. - by rewrite big_nil; exact/Rle_refl. - apply (@leR_trans (F hd)); last by rewrite big_cons; exact: leR_maxl. by apply: Hr; rewrite in_cons eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)