proposition: Lemma sub_le_big_seq (I : eqType) s s' P (F : I -> R) : (forall i, count_mem i s <= count_mem i s')%N -> le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s' | P i) F i).
proof: Proof. rewrite (big_AC_mk_monoid opA opC) => /count_subseqP[_ /subseqP[m sm ->]]. move/(perm_big _)->; rewrite big_mask big_tnth. by rewrite -!(big_AC_mk_monoid opA opC) sub_le_big // => j /andP[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)