proposition: Lemma eq_bigmin j P F : P j -> (forall i, P i -> F i <= x) -> {i0 | i0 \in P & \big[min/x]_(i | P i) F i = F i0}.
proof: Proof. by move=> Pi0 Hx; rewrite (bigmin_eq_arg Pi0) //; eexists=> //; case: arg_minP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)