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

State before:
a : ℤ
n : ℕ
⊢ mod2 (-mod2 a n) n = mod2 (-a) n
Tactic:
sorry
State after:
no goals