src/HOL/Binomial.thy

 
 lemma binomial_code [code]:
   "n choose k =
       (if k > n then 0
        else if 2 * k > n then n choose (n - k)
-       else (fold_atLeastAtMost_nat ( * ) (n - k + 1) n 1 div fact k))"
+       else (fold_atLeastAtMost_nat (*) (n - k + 1) n 1 div fact k))"
 proof -
   {
     assume "k \<le> n"
     then have "{1..n} = {1..n-k} \<union> {n-k+1..n}" by auto
     then have "(fact n :: nat) = fact (n-k) * \<Prod>{n-k+1..n}"