. have h: (n / 2^sz % 2 = 0) ∨ (n / 2^sz %2 = 1) := by sorry
  match h with
  | .inl h => simp [h, ih]; sorry_arith
  | .inr h => simp [h, ih]; sorry_arith
case left
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz)

case right
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz
case right
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz