proposition: Lemma sub_in_bigmin [x0] [I : eqType] (r : seq I) (P P' : {pred I}) F : {in r, forall i, P' i -> P i} -> \big[min/x0]_(i <- r | P i) F i <= \big[min/x0]_(i <- r | P' i) F i.
proof: Proof. exact: (sub_in_le_big 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)