by_cases hN : N=0
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
⊢ a ∣ b
case pos
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
hN : N = 0
⊢ a ∣ b

case neg
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
hN : ¬N = 0
⊢ a ∣ b