proposition: Lemma bigmax_leP m P F : reflect (x <= m /\ forall i, P i -> F i <= m) (\big[max/x]_(i | P i) F i <= m).
proof: Proof. apply: (iffP idP) => [|[? ?]]; last exact: bigmax_le. rewrite bigmax_idl ge_max => /andP[-> leFm]; split=> // i Pi. by apply: le_trans leFm; exact: le_bigmax_cond. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)