case succ sz ih =>
  simp [FinInt.ofIntAux, ih]; constructor
  . 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
  . sorry_arith
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
no goals