have : m > 0 := Nat.pos_of_ne_zero hm
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
⊢ (if n = 0 then if flip f true false = true then m else 0
    else
      if flip f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then
        bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2) + 1
      else bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2)) =
    if n = 0 then if f false true = true then m else 0
    else
      if f (decide (n % 2 = 1)) (decide (m % 2 = 1)) = true then
        bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
      else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
this : m > 0
⊢ (if n = 0 then if flip f true false = true then m else 0
    else
      if flip f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then
        bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2) + 1
      else bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2)) =
    if n = 0 then if f false true = true then m else 0
    else
      if f (decide (n % 2 = 1)) (decide (m % 2 = 1)) = true then
        bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
      else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)