proposition: Lemma bigmax_sup (I : finType) i0 (P : pred I) m F : P i0 -> m <= F i0 -> m <= \max_(i | P i) F i.
proof: Proof. by move=> Pi0 le_m_Fi0; apply: leq_trans (leq_bigmax_cond i0 Pi0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)