simp [if_neg hn]
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ getBit
      (if n = 0 then if f true false = true then m else 0
      else
        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))
      0 =
    f (getBit m 0) (getBit n 0)
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ getBit
      (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))
      0 =
    f (getBit m 0) (getBit n 0)