proposition: Lemma subset_bigmin_cond [x0] (I : finType) (A A' P P' : {pred I}) (F : I -> T) : [set i in A' | P' i] \subset [set i in A | P i] -> \big[min/x0]_(i in A | P i) F i <= \big[min/x0]_(i in A' | P' i) F i.
proof: Proof. exact: (subset_le_big_cond ge_refl). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)