proposition: Lemma eq_bigmax_cond (I : finType) (A : pred I) F : #|A| > 0 -> {i0 | i0 \in A & \max_(i in A) F i = F i0}.
proof: Proof. case: (pickP A) => [i0 Ai0 _ | ]; last by move/eq_card0->. by exists [arg max_(i > i0 in A) F i]; [case: arg_maxnP | apply: bigmax_eq_arg]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)