proposition: Lemma bigmin_inf i0 (P : pred I) (m : 'I_n.+1) F : P i0 -> m >= F i0 -> m >= \min_(i | P i) F i.
proof: Proof. by move=> Pi0 le_m_Fi0; apply: leq_trans (geq_bigmin_cond i0 Pi0) _. Qed.
imports: HB(structures) mathcomp(all_ssreflect)