proposition: Lemma bigmax_leqP (I : finType) (P : pred I) m F : reflect (forall i, P i -> F i <= m) (\max_(i | P i) F i <= m).
proof: Proof. apply: (iffP idP) => leFm => [i Pi|]. by apply: leq_trans leFm; apply: leq_bigmax_cond. by elim/big_ind: _ => // m1 m2; rewrite geq_max => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)