proposition: Lemma bigmaxR_eq (A : finType) (C : {set A}) a (f : A -> R): a \in C -> (forall a0, 0 <= f a0) -> (forall c, c \in C -> f c <= f a) -> f a = \rmax_(c | c \in C) f c.
proof: Proof. move=> aC f0 Hf. rewrite -big_filter. apply bigmaxR_seq_eq => //. - by rewrite mem_filter aC /= mem_index_enum. - by move=> a0; rewrite mem_filter mem_index_enum andbT => /Hf. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)