proposition: Lemma bigmaxR_perm (I : eqType) g : forall (s1 s2 : seq I), (forall r, r \in s2 -> 0 <= g r) -> perm_eq s1 s2 -> uniq s1 -> uniq s2 -> \rmax_(c0 <- s1) g c0 = \rmax_(c0 <- s2) g c0.
proof: Proof. move=> s1. move H : (size s1) => n1. elim: n1 s1 H => //. case=> // _ s _ Hs. suff -> : s = [::]. move=> _ _; by rewrite !big_nil. destruct s => //. move/allP : Hs. move/(_ s). by rewrite /= inE eqxx /= => /(_ Logic.eq_refl) /= add1n. move=> n1 IH1 [|h1 t1] // [] H1 s2 Hg Hs2 K1 K2. rewrite big_cons. have [h2 [t2 ht2]] : exists h2 t2, s2 = h2 ++ h1 :: t2. have /path.splitPr[h2 t2] : h1 \in s2 by rewrite -(perm_mem Hs2) in_cons eqxx. by exists h2, t2. have Hs2' : perm_eq t1 (h2 ++ t2). rewrite ht2 in Hs2. rewrite -(perm_cons h1). eapply perm_trans; first by apply Hs2. by rewrite perm_catC /= perm_cons perm_catC. have Hg' r : r \in h2 ++ t2 -> 0 <= g r. move=> rs2; apply Hg. rewrite ht2 mem_cat in_cons. rewrite mem_cat in rs2. case/orP : rs2 => [-> // | -> /=]. by rewrite orbA orbC. rewrite (IH1 _ H1 _ Hg' Hs2'); last 2 first. by case/andP : K1. rewrite ht2 cat_uniq /= in K2. case/andP : K2 => K2 /andP [] K4 /andP [] _ K3. rewrite cat_uniq K2 K3 /= andbC /=. rewrite negb_or in K4. by case/andP : K4. rewrite bigmaxR_cat // maxRA (maxRC (g h1)) -maxRA ht2 bigmaxR_cat; last first. move=> x Hx; apply Hg; by rewrite ht2. by rewrite big_cons. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)