proposition: Lemma multinomial_filter_neq0 s : 'C[[seq i <- s | i != 0]] = 'C[s].
proof: Proof. rewrite !multinomial_factd; congr (_ %/ _). - congr (_`!); elim: s => [| s0 s IHs] //=. by case: eqP => [-> | _] /=; rewrite ?add0n IHs. - rewrite big_filter [RHS](bigID (fun i => i == 0)) /=. by rewrite [X in X * _]big1 ?mul1n // => i /eqP ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(bigop div binomial) tools