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

State before:
p : ℕ
h : p.Prime
k : ℕ
⊢ ∀ r < p, ¬p ∣ (p * k + r).descFactorial r
Tactic:
refine Nat.rec (λ _ ↦ h.not_dvd_one) (λ r h0 h1 ↦ ?_)
State after:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ (p * k + r.succ).descFactorial r.succ

State before:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ (p * k + r.succ).descFactorial r.succ
Tactic:
rw [Nat.add_succ, Nat.succ_descFactorial_succ]
State after:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ (p * k + r + 1) * (p * k + r).descFactorial r

State before:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ (p * k + r + 1) * (p * k + r).descFactorial r
Tactic:
refine h.not_dvd_mul ?_ (h0 <| r.lt_succ_self.trans h1)
State after:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ p * k + r + 1

State before:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ p * k + r + 1
Tactic:
rw [add_assoc, Nat.dvd_add_right ⟨k, rfl⟩]
State after:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ r + 1

State before:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ r + 1
Tactic:
exact Nat.not_dvd_of_pos_of_lt r.succ_pos h1
State after:
no goals