proposition: Lemma bigmax_imset [I J : finType] x [h : I -> J] [A : {set I}] (F : J -> T) : \big[max/x]_(j in [set h x | x in A]) F j = \big[max/x]_(i in A) F (h i).
proof: Proof. by apply: big_imset_idem; apply: maxxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)