proposition: Lemma bigmaxR_bigmin_vec (A M : finType) n (f : {ffun M -> 'rV[A]_n}) (g : nat -> R) (cnot0 : {c0 | c0 \in f @: M } ) : (forall n1 n2, (n1 <= n2 <= n)%nat -> (g n2 <= g n1)%R) -> (forall r, 0 <= g r) -> forall m (d : 'rV[A]_n -> nat) (_ : forall c0 : 'rV[A]_n, c0 \in f @: M -> (d c0 <= n)%nat), d (f m) = \min^ (sval cnot0) _(c in f @: M) d c -> g (d (f m)) = \rmax_(m in M) g (d (f m)).
proof: Proof. move=> n1n2 Hg m d H Hd. transitivity (\rmax_(c in f @: M) g (d c)); last by rewrite bigmaxR_imset. apply bigmaxR_bigmin_vec_helper with cnot0 => //. by apply/imsetP; exists m. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct) mathcomp(matrix)