proposition: Lemma bigmax_eq_arg (I : finType) i0 (P : pred I) F : P i0 -> \max_(i | P i) F i = F [arg max_(i > i0 | P i) F i].
proof: Proof. move=> Pi0; case: arg_maxnP => //= i Pi maxFi. by apply/eqP; rewrite eqn_leq leq_bigmax_cond // andbT; apply/bigmax_leqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)