proposition: Lemma subset_le_big_cond (I : finType) (A A' P P' : {pred I}) (F : I -> R) : [set i in A | P i] \subset [set i in A' | P' i] -> le (\big[op/x]_(i in A | P i) F i) (\big[op/x]_(i in A' | P' i) F i).
proof: Proof. by move=> /subsetP AP; apply: sub_le_big => // i; have /[!inE] := AP i. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)