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

State before:
n : ℕ
a b : ℤ
⊢ a ≡ b [2^n] → a ≡ mod2 b n [2^n]
Tactic:
simp [cong2, mod2_idem mod2_bounds]
State after:
no goals