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

State before:
a : ℤ
n : ℕ
⊢ smod2 a n = mod2 (a + 2 ^ n) (n + 1) - 2 ^ n
Tactic:
sorry
State after:
no goals