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

State before:
x : ℤ
n : ℕ
⊢ mod2 (x + 2 ^ n) n = mod2 x n
Tactic:
sorry
State after:
no goals