proposition: Lemma bigmax_eq_arg j P F : P j -> (forall i, P i -> x <= F i) -> \big[max/x]_(i | P i) F i = F [arg max_(i > j | P i) F i].
proof: Proof. move=> Pi0; case: arg_maxP => //= i Pi PF PxF. apply/eqP; rewrite eq_le le_bigmax_cond // andbT. by apply/bigmax_leP; split => //; exact: PxF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)