Theorem: FinInt.toSint_ofSint (MLIR/Util/FinInt.lean)

State before:
sz : ℕ
n : ℤ
⊢ toSint (ofInt (sz + 1) n) = smod2 n sz
Tactic:
sorry
State after:
no goals