simp [FinInt.ofIntAux, ih]
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (FinInt.ofIntAux (Nat.succ sz) n).fst = mod2 n (Nat.succ sz) ∧
    (FinInt.ofIntAux (Nat.succ sz) n).snd = n / 2 ^ Nat.succ sz
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) ∧
    n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz