proposition: Lemma bigmin_le_cond j P F : P j -> \big[min/x]_(i | P i) F i <= F j.
proof: Proof. have := mem_index_enum j; rewrite unlock; elim: (index_enum I) => //= i l ih. rewrite inE => /orP [/eqP-> ->|/ih leminlfi Pi]; first by rewrite ge_min lexx. by case: ifPn => Pj; [rewrite ge_min leminlfi// orbC|exact: leminlfi]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)