rw [←Nat.mul_two, Nat.pow_succ]
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then bitwise f (m / 2) (n / 2) + bitwise f (m / 2) (n / 2) + 1
    else bitwise f (m / 2) (n / 2) + bitwise f (m / 2) (n / 2)) <
    2 ^ succ k
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then bitwise f (m / 2) (n / 2) * 2 + 1
    else bitwise f (m / 2) (n / 2) * 2) <
    2 ^ k * 2