proposition: Lemma bigmax_sup_seq (I : eqType) r i0 (P : pred I) m F : i0 \in r -> P i0 -> m <= F i0 -> m <= \max_(i <- r | P i) F i.
proof: Proof. by move=> i0r Pi0 ?; apply: leq_trans (leq_bigmax_seq i0 _ _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)