proposition: Lemma bigmin_geqP (P : pred I) (m : 'I_n.+1) F : reflect (forall i, P i -> F i >= m) (\min_(i | P i) F i >= m).
proof: Proof. apply: (iffP idP) => leFm => [i Pi|]. by apply: leq_trans leFm _; apply: geq_bigmin_cond. by elim/big_ind: _; rewrite ?leq_ord // => m1 m2; rewrite leq_min => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect)