aesop
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
this : 1 ≤ m
⊢ ((1 ≤ m ∧ ↑m < √↑N) ∧ k ≤ Nat.log 2 N) ∧ m ^ k = n
no goals