fact: Fixpoint binomial (n k : nat) : nat := match n with | 0 => match k with | 0 => 1 | S _ => 0 end | S n' => match k with | 0 => 1 | S k' => (binomial n' k') + (binomial n' k) end end.
imports: Arith ZArith String List Psatz Factorial