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

State before:
n : ℕ
a : ℤ
⊢ a ≥ -2 ^ n ∧ a < 2 ^ n → smod2 a n = a
Tactic:
sorry
State after:
no goals