proposition: Lemma bigmin_gtP 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: lt_bigmin]. - by rewrite (lt_le_trans lemFi)// bigmin_idl ge_min lexx. - by move=> i Pi; rewrite (lt_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)