n : Nat
h✝ : isPowerOfTwo n
k : Nat
h : n = 2 ^ k
⊢ n > 0
n : Nat
h : isPowerOfTwo n
⊢ n > 0
have ⟨k, h⟩ := h
n : Nat
h✝ : isPowerOfTwo n
k : Nat
h : n = 2 ^ k
⊢ 2 ^ k > 0
n : Nat
h✝ : isPowerOfTwo n
k : Nat
h : n = 2 ^ k
⊢ n > 0
rw [h]
case h
n : Nat
h✝ : isPowerOfTwo n
k : Nat
h : n = 2 ^ k
⊢ 0 < 2
n : Nat
h✝ : isPowerOfTwo n
k : Nat
h : n = 2 ^ k
⊢ 2 ^ k > 0
apply Nat.pos_pow_of_pos
no goals
case h
n : Nat
h✝ : isPowerOfTwo n
k : Nat
h : n = 2 ^ k
⊢ 0 < 2
decide