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

State before:
sz₁ sz₂ : ℕ
n : FinInt sz₁
⊢ toUint (zext sz₂ n) = mod2 (toUint n) sz₂
Tactic:
simp [zext, toUint_ofInt]
State after:
no goals