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

State before:
sz : ℕ
n : FinInt sz
⊢ toUint (-n) ≡ -toUint n [2^sz]
Tactic:
simp [cong2, toUint_mod2]
State after:
sz : ℕ
n : FinInt sz
⊢ toUint (-n) = mod2 (-toUint n) sz

State before:
sz : ℕ
n : FinInt sz
⊢ toUint (-n) = mod2 (-toUint n) sz
Tactic:
apply neg_toUint
State after:
no goals