proposition: Lemma leR_bigmaxRl (A : finType) (f : A -> R) (s : seq A) a : (forall a0, 0 <= f a0) -> (forall a0, a0 \in s -> f a0 <= f a) -> \rmax_(a0 <- s) f a0 <= f a.
proof: Proof. elim: s a => [a f0 _ | a0 s' IH a f0 Hf]. rewrite big_nil; exact/f0. rewrite big_cons; apply Rmax_lub. - by apply Hf; rewrite mem_head. - apply IH => // a1 a1s; apply Hf. by rewrite in_cons a1s orbC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)