rw [two_mul, add_assoc]
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
case a.div
m p : ℕ
ha : m + 1 < p
hb : p ≤ 2 * m + 1
hp : Nat.Prime p
⊢ p ∣ Nat.choose (m + (m + 1)) m