Binomial coefficients and consecutive products

This file contains results relating divisibility of binomial coefficients to divisibility of consecutive products.

theorem Nat.Prime.dvd_choose_add_sub_one_iff {p k n : ℕ} (hp : Prime p) (hpn : n < p) : p ∣ (k + n - 1).choose n ↔ ∃ i < n, p ∣ k + i

theorem Nat.Prime.dvd_choose_iff {p k n : ℕ} (hp : Prime p) (hpn : n < p) (hnk : n ≤ k) : p ∣ k.choose n ↔ ∃ i < n, p ∣ k - i