proposition: Lemma bigmaxR_imset (M I : finType) h (g : I -> R) : (forall r : I, r \in [set h x | x in M] -> 0 <= g r) -> \rmax_(c0 in [set h x | x in M]) g c0 = \rmax_(m in M) g (h m).
proof: Proof. move=> Hg. eapply trans_eq. eapply trans_eq; last first. apply (@bigmaxR_imset_helper _ I h g (enum M)). move=> r; rewrite mem_enum; case/imsetP => x; rewrite mem_enum => Hx ->. apply Hg; apply/imsetP; by exists x. rewrite big_filter /=. apply congr_big => //. move=> i /=. move Hlhs : (i \in _) => lhs. destruct lhs. - case/imsetP : Hlhs => x Hx ?; subst i. symmetry; apply/imsetP. exists x => //. by rewrite mem_enum. - symmetry. apply/negbTE. move/negbT : Hlhs; apply contra. case/imsetP => m Hm ?; subst i. apply/imsetP. by exists m. apply congr_big => //; by rewrite enumT. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)