proposition: Lemma bigmin_eq_arg j P F : P j -> (forall i, P i -> F i <= x) -> \big[min/x]_(i | P i) F i = F [arg min_(i < j | P i) F i].
proof: Proof. move=> Pi0; case: arg_minP => //= i Pi PF PFx. apply/eqP; rewrite eq_le bigmin_le_cond //=. by apply/bigmin_geP; split => //; exact: PFx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)