proposition: Lemma bigmaxR_imset_helper (M I : finType) h (g : I -> R) (s : seq M) : (forall r : I, r \in enum [set h x | x in s] -> 0 <= g r) -> \rmax_(c0 <- enum [set h x | x in s]) g c0 = \rmax_(m <- s) g (h m).
proof: Proof. elim: s => [|hd tl IH Hg /=]. rewrite big_nil. set tmp := enum _. suff -> : tmp = [::] by rewrite big_nil. rewrite /tmp -[in X in _ = X]enum0. apply eq_enum => a. rewrite !inE. apply/imsetP. case => m. by rewrite in_nil. rewrite big_cons -IH; last first. move=> r Hr. apply Hg. rewrite mem_enum. apply/imsetP. rewrite mem_enum in Hr. case/imsetP : Hr => x xtl Hr. exists x => //. by rewrite in_cons xtl orbC. transitivity (\rmax_(c0 <- h hd :: enum [set h x | x in tl]) g c0). apply bigmaxR_eqi => // x. rewrite inE !mem_enum. move Hlhs : (x \in [set _ _ | _ in _]) => lhs. destruct lhs. - case/imsetP : Hlhs => x0 Hx0 H. rewrite in_cons in Hx0. case/orP : Hx0 => Hx0. move/eqP : Hx0 => ?; subst x0. by rewrite H eqxx. symmetry. apply/orP; right. apply/imsetP; by exists x0. - symmetry. apply/negbTE. move/negbT : Hlhs. apply contra. case/orP => Hcase. + move/eqP in Hcase; subst x. apply/imsetP. exists hd => //. by rewrite inE eqxx. + apply/imsetP. case/imsetP : Hcase => x0 Hx0 ?; subst x. exists x0 => //. by rewrite inE Hx0 orbC. by rewrite big_cons. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)