proposition: Lemma sub_le_big_seq_cond (I : eqType) s s' P P' (F : I -> R) : (forall i, count_mem i (filter P s) <= count_mem i (filter P' s'))%N -> le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s' | P' i) F i).
proof: Proof. by move=> /(sub_le_big_seq xpredT F); rewrite !big_filter. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)