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

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