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