[GOAL]
p a b k : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
⊢ p ∣ choose (a + b) a
[PROOFSTEP]
have h₁ : p ∣ (a + b)! := hp.dvd_factorial.2 h
[GOAL]
p a b k : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : p ∣ (a + b)!
⊢ p ∣ choose (a + b) a
[PROOFSTEP]
rw [← add_choose_mul_factorial_mul_factorial, ← choose_symm_add, hp.dvd_mul, hp.dvd_mul, hp.dvd_factorial,
  hp.dvd_factorial] at h₁ 
[GOAL]
p a b k : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : (p ∣ choose (a + b) a ∨ p ≤ a) ∨ p ≤ b
⊢ p ∣ choose (a + b) a
[PROOFSTEP]
exact (h₁.resolve_right hbp.not_le).resolve_right hap.not_le
