proposition: Lemma bigmin_geP m P F : reflect (m <= x /\ forall i, P i -> m <= F i) (m <= \big[min/x]_(i | P i) F i).
proof: Proof. apply: (iffP idP) => [lemFi|[lemx lemPi]]; [split|exact: le_bigmin]. - by rewrite (le_trans lemFi)// bigmin_idl ge_min lexx. - by move=> i Pi; rewrite (le_trans lemFi)// (bigminD1 _ Pi)// le_minl lexx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)