theorem Nat.binom_symmetric {n k : Nat} (h : k ≤ n) : n.binom k = n.binom (n - k)

@[simp]

theorem Nat.binom_self (n : Nat) : n.binom n = 1

theorem Nat.sum_binom {n : Nat} : Nat.sum_ft 0 (n + 1) n.binom = 2 ^ n

theorem Nat.binom_succ_succ_of_le {n k : Nat} (h : k + 1 ≤ n) : (n + 1).binom (k + 1) = n.binom (k + 1) + n.binom k

@[simp]

theorem Nat.binom_succ_succ {n k : Nat} : (n + 1).binom (k + 1) = n.binom (k + 1) + n.binom k

@[simp]

theorem Nat.binom_zero_succ {k : Nat} : Nat.binom 0 (k + 1) = 0

@[simp]

theorem Nat.binom_zero {n : Nat} : n.binom 0 = 1

theorem Nat.factorial_eq_binom_mul {n : Nat} (k : Nat) (h : k ≤ n) : n.binom k * k.factorial * (n - k).factorial = n.factorial

@[simp]

theorem Nat.binom_one {n : Nat} : n.binom 1 = n

@[simp]

theorem Nat.binom_two {n : Nat} : n.binom 2 = n * (n - 1) / 2