proposition: Lemma prod_seq_count (s : seq T) (F : T -> R) : \prod_(i <- s) F i = \prod_(i <- (undup s)) ((F i) ^+ (count (xpred1 i) s)).
proof: Proof. elim: s=> /= [|a l IHl]; first by rewrite !big_nil. rewrite big_cons IHl. set r:= if _ then _ else _. have ->: \big[*%R/1]_(i <- r) (F i) ^+ ((a == i) + count (eq_op^~ i) l) = \big[*%R/1]_(i <- r) (F i) ^+ (a == i) * \big[*%R/1]_(i <- r) (F i) ^+ (count (eq_op^~ i) l). by rewrite -big_split /=; apply: eq_bigr=> i _; rewrite exprD. have ->: \big[*%R/1]_(i <- r) (F i) ^+ (a == i) = F a. rewrite /r; case: ifP=>[|notal]. rewrite -mem_undup=> aundl. rewrite (bigD1_seq _ aundl (undup_uniq l)) /= eqxx big1 ?mulr1 //. by move=> i /negbTE neqai; rewrite eq_sym neqai. rewrite big_cons eqxx big1_seq ?mulr1 // => i /= iundl. case: (eqVneq a i) => //= eqai. by rewrite eqai -mem_undup iundl in notal. rewrite /r; case: ifP=> // /negbT notal. rewrite big_cons. have->: count (xpred1 a) l = 0%N. by apply/eqP; rewrite -leqn0 leqNgt -has_count has_pred1. by rewrite mul1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype finfun perm matrix bigop zmodp mxalgebra) mathcomp(choice poly polydiv mxpoly binomial)