by_cases hd' : d = 0
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ 2 ≤ d
case pos
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : d = 0
⊢ 2 ≤ d

case neg
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : ¬d = 0
⊢ 2 ≤ d