Divisibility properties of binomial coefficients

theorem Nat.Prime.dvd_choose_add {p : ℕ} {a : ℕ} {b : ℕ} (hp : Nat.Prime p) (hap : a < p) (hbp : b < p) (h : p ≤ a + b) : p ∣ (a + b).choose a

theorem Nat.Prime.dvd_choose {p : ℕ} {a : ℕ} {b : ℕ} (hp : Nat.Prime p) (ha : a < p) (hab : b - a < p) (h : p ≤ b) : p ∣ b.choose a

theorem Nat.Prime.dvd_choose_self {p : ℕ} {k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) (hkp : k < p) : p ∣ p.choose k