From Corelib Require Import Setoid.
From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype fintype choice seq.
From mathcomp Require Import bigop div binomial.

Require Import tools.

Set Implicit Arguments.

Implicit Type (i a b : nat) (s t : seq nat).

Fixpoint multinomial_rec s :=
  if s is i :: s' then 'C(sumn s, i) * (multinomial_rec s') else 1.
Arguments multinomial_rec : simpl nomatch.
Definition multinomial := multinomial_rec.
Arguments multinomial : simpl never.
Notation "''C' [ s ]" := (multinomial s)
  (at level 0, format "''C' [ s ]") : nat_scope.

Lemma multinomial0 : 'C[[::]] = 1.
Lemma multinomial1 i : 'C[[:: i]] = 1.
Lemma multinomialE i s : 'C[i :: s] = 'C(i + sumn s, i) * 'C[s].
Lemma multinomial2 a b : 'C[[:: a; b]] = 'C(a + b, a).

Lemma multinomial_fact s : 'C[s] * \prod_(i <- s) i`! = (sumn s)`!.

Lemma multinomial_nseq n a : 'C[nseq n a] * (a`! ^ n) = (a * n)`!.

Lemma multinomial_nseq1 n : 'C[nseq n 1] = n`!.

Lemma dvdn_prodfact s : \prod_(i <- s) i`! %| (sumn s)`! .

Lemma multinomial_factd s : 'C[s] = (sumn s)`! %/ \prod_(i <- s) i`!.

Lemma multinomial_cat s t :
  'C[s ++ t] = 'C(sumn s + sumn t, sumn s) * 'C[s] * 'C[t].

Lemma perm_multinomial s t : perm_eq s t -> 'C[s] = 'C[t].

Lemma multinomial_filter_neq0 s : 'C[[seq i <- s | i != 0]] = 'C[s].