intro p ha hb hp
case a.div
m : ℕ
⊢ ∀ (a : ℕ), m + 1 < a → a ≤ 2 * m + 1 → Nat.Prime a → a ∣ Nat.choose (2 * m + 1) m
case a.div
m p : ℕ
ha : m + 1 < p
hb : p ≤ 2 * m + 1
hp : Nat.Prime p
⊢ p ∣ Nat.choose (2 * m + 1) m