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 ∣ Nat.choose (a + b) a

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

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