exact Nat.pos_pow_of_pos k.succ (Nat.zero_lt_succ 1)
case refl.false
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ 0 < 2 ^ succ k
no goals