m n : ℕ
h : n ≤ m
p : ℕ
hp : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p
⊢ p ∣ Nat.choose (m + n) m
m n : ℕ
h : n ≤ m
p : ℕ
hp : p ∈ filter Nat.Prime (Ico (m + 1) (m + n + 1))
⊢ p ∣ Nat.choose (m + n) m
rw [mem_filter, mem_Ico] at hp
no goals
m n : ℕ
h : n ≤ m
p : ℕ
hp : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p
⊢ p ∣ Nat.choose (m + n) m
exact hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1))
    (Nat.lt_succ_iff.1 hp.1.2)