apply Finset.prod_primes_dvd <;> simp [← Nat.prime_iff]
case a
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ∣ Nat.choose (2 * m + 1) m
case a.div
m : ℕ
⊢ ∀ (a : ℕ), m + 1 < a → a ≤ 2 * m + 1 → Nat.Prime a → a ∣ Nat.choose (2 * m + 1) m