. calc
  bitwise f (m/2) (n/2) * 2 + 1 
    < bitwise f (m/2) (n/2) * 2 + 2 := Nat.lt_succ_self _
  _ = (bitwise f (m/2) (n/2)) * 2 + 1*2 := rfl
  _ = (bitwise f (m/2) (n/2) + 1) * 2 := (Nat.add_mul _ _ 2).symm
  _ ≤ 2^k * 2 := Nat.mul_le_mul_right 2 (h_ind ‹m/2 < 2^k› ‹n/2 < 2^k›)
case true
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
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ bitwise f (m / 2) (n / 2) * 2 + 1 < 2 ^ k * 2
no goals