proposition: Lemma uniq_sub_le_big (I : eqType) s s' P (F : I -> R) : uniq s -> uniq s' -> {subset s <= s'} -> le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s' | P i) F i).
proof: Proof. move=> us us' ss'; rewrite sub_le_big_seq => // i; rewrite !count_uniq_mem//. by have /implyP := ss' i; case: (_ \in s) (_ \in s') => [] []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)