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

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