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

State before:
sz n : ℕ
⊢ toUint (OfNat.ofNat n) = mod2 (↑n) sz
Tactic:
simp [OfNat.ofNat, toUint_ofInt]
State after:
no goals