Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import 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 := nosimpl multinomial_rec.
Notation "''C' [ s ]" := (multinomial s)
  (at level 8, 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].