fact: Fixpoint Nsimple_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' => (Nsimple_binomial n' k') + (Nsimple_binomial n' k) end end.
imports: Arith Compare Nfinite_prod Ndiv