no goals
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : m < p → m ∣ p → m = 1
m2 : 2 ≤ m
l : m < p
d : m ∣ p
⊢ 1 < 2
decide
case zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ zero → zero < p → ¬zero ∣ p
l : zero < p
d : zero ∣ p
⊢ zero = 1

case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ succ zero → succ zero < p → ¬succ zero ∣ p
l : succ zero < p
d : succ zero ∣ p
⊢ succ zero = 1

case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ succ (succ m) → succ (succ m) < p → ¬succ (succ m) ∣ p
l : succ (succ m) < p
d : succ (succ m) ∣ p
⊢ succ (succ m) = 1
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m → m < p → ¬m ∣ p
l : m < p
d : m ∣ p
⊢ m = 1
rcases m with (_ | _ | m)
case zero
p : ℕ
p2 : 2 ≤ 0
h : 2 ≤ zero → zero < p → ¬zero ∣ p
l : zero < p
d : zero ∣ p
⊢ zero = 1
case zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ zero → zero < p → ¬zero ∣ p
l : zero < p
d : zero ∣ p
⊢ zero = 1
rw [eq_zero_of_zero_dvd d] at p2
case zero
p : ℕ
h : 2 ≤ zero → zero < p → ¬zero ∣ p
l : zero < p
d : zero ∣ p
⊢ 2 ≤ 0 → zero = 1
case zero
p : ℕ
p2 : 2 ≤ 0
h : 2 ≤ zero → zero < p → ¬zero ∣ p
l : zero < p
d : zero ∣ p
⊢ zero = 1
revert p2
no goals
case zero
p : ℕ
h : 2 ≤ zero → zero < p → ¬zero ∣ p
l : zero < p
d : zero ∣ p
⊢ 2 ≤ 0 → zero = 1
decide
no goals
case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ succ zero → succ zero < p → ¬succ zero ∣ p
l : succ zero < p
d : succ zero ∣ p
⊢ succ zero = 1
rfl
no goals
case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ succ (succ m) → succ (succ m) < p → ¬succ (succ m) ∣ p
l : succ (succ m) < p
d : succ (succ m) ∣ p
⊢ succ (succ m) = 1
exact (h le_add_self l).elim d