Theorem: IMOSL.IMO2012N3.prime_binom_not_dvd (IMOSLLean4/IMO2012/N3/N3.lean)

State before:
k p : ℕ
h : p.Prime
h0 : k ≠ 0
h1 : p * k ∣ (p * k).choose p
⊢ False
Tactic:
apply prime_not_dvd_descFactorial h k.pred p.pred (p.pred_lt_self h.pos)
State after:
k p : ℕ
h : p.Prime
h0 : k ≠ 0
h1 : p * k ∣ (p * k).choose p
⊢ p ∣ (p * k.pred + p.pred).descFactorial p.pred

State before:
k p : ℕ
h : p.Prime
h0 : k ≠ 0
h1 : p * k ∣ (p * k).choose p
⊢ p ∣ (p * k.pred + p.pred).descFactorial p.pred
Tactic:
rw [← Nat.mul_dvd_mul_iff_left (p * k.pred + p.pred).succ_pos,
  ← Nat.succ_descFactorial_succ, ← Nat.succ_eq_add_one, ← Nat.add_succ,
  ← Nat.succ_eq_add_one, Nat.succ_pred h.ne_zero, ← p.mul_succ,
  Nat.succ_pred h0, Nat.descFactorial_eq_factorial_mul_choose, mul_comm]
State after:
k p : ℕ
h : p.Prime
h0 : k ≠ 0
h1 : p * k ∣ (p * k).choose p
⊢ p * (p * k) ∣ p.factorial * (p * k).choose p

State before:
k p : ℕ
h : p.Prime
h0 : k ≠ 0
h1 : p * k ∣ (p * k).choose p
⊢ p * (p * k) ∣ p.factorial * (p * k).choose p
Tactic:
exact mul_dvd_mul (Nat.dvd_factorial h.pos p.le_refl) h1
State after:
no goals