proposition: Lemma bigmaxR_eqi (I : finType) g (s1 s2 : seq I) : (forall r : I, r \in s1 -> 0 <= g r) -> s1 =i s2 -> \rmax_(c0 <- s1) g c0 = \rmax_(c0 <- s2) g c0.
proof: Proof. move=> Hg s1s2. rewrite (bigmaxR_undup _ _ s1) (bigmaxR_undup _ g s2). apply bigmaxR_perm; [ | | by rewrite undup_uniq | by rewrite undup_uniq]. - move=> r Hr; apply Hg. rewrite mem_undup in Hr. by rewrite s1s2. - apply uniq_perm; [by rewrite undup_uniq | by rewrite undup_uniq | ]. move=> i; by rewrite !mem_undup. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)