proposition: Lemma bigmaxR_bigmin_vec_helper (A : finType) n (g : nat -> R) : (forall n1 n2, (n1 <= n2 <= n)%nat -> (g n2 <= g n1)%R) -> (forall r, 0 <= g r) -> forall (C : {set 'rV[A]_n}) c (_ : c \in C) (d : 'rV[A]_n -> nat) (_ : forall c, c \in C -> (d c <= n)%nat) (cnot0 : {c0 | c0 \in C}), d c = \min^ (sval cnot0) _(c in C) d c -> g (d c) = \rmax_(c in C) g (d c).
proof: Proof. move=> Hdecr Hr C c cC d Hd cnot0 H. apply (@bigmaxR_eq _ C c (fun a => g (d a))) => //. move=> /= c0 c0C. apply/Hdecr/andP; split; [|exact: Hd]. rewrite H; exact: leq_bigmin. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct) mathcomp(matrix)