proposition: Lemma bigmaxR_cat (I : eqType) g : forall (s1 s2 : seq I), (forall x, x \in s1 ++ s2 -> 0 <= g x) -> \rmax_(c <- s1 ++ s2) g c = Rmax (\rmax_(c <- s1) g c) (\rmax_(c <- s2) g c).
proof: Proof. elim => [s2 Hg /= | h1 t1 IH s2 Hg /=]. by rewrite big_nil Rmax_right //; exact: bigmaxR_ge0. rewrite 2!big_cons IH ?maxRA // => x Hx; apply: Hg. by rewrite /= in_cons Hx orbC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)