Divisibility properties of binomial coefficients

theorem Nat.Prime.dvd_choose_add {p a b : ℕ} (hp : 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 : 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 : Prime p) (hk : k ≠ 0) (hkp : k < p) : p ∣ p.choose k

theorem Nat.Prime.coprime_choose_of_lt {p a b : ℕ} (hp : Prime p) (hb : b < p) (ha : a ≤ b) : p.Coprime (b.choose a)