. simp [mod2_idem ⟨Int.add_ge_zero _ _ toUint_ge toUint_ge, by assumption⟩]
case inl
sz : ℕ
n m : FinInt sz
h✝ : toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m = mod2 (toUint n + toUint m) sz

case inr
sz : ℕ
n m : FinInt sz
h✝ : ¬toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m - 2 ^ sz = mod2 (toUint n + toUint m) sz
case inr
sz : ℕ
n m : FinInt sz
h✝ : ¬toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m - 2 ^ sz = mod2 (toUint n + toUint m) sz