dsimp [getBit]
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then getBit (1 + bitwise f (m / 2) (n / 2) * 2) 0
    else getBit (bitwise f (m / 2) (n / 2) * 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
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then decide ((1 + bitwise f (m / 2) (n / 2) * 2) % 2 = 1)
    else decide (bitwise f (m / 2) (n / 2) * 2 % 2 = 1)) =
    f (decide (m % 2 = 1)) (decide (n % 2 = 1))