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

State before:
a : ℤ
n : ℕ
⊢ mod2 a n < 2 ^ n
Tactic:
simp [mod2]
State after:
a : ℤ
n : ℕ
⊢ a % 2 ^ n < 2 ^ n

State before:
a : ℤ
n : ℕ
⊢ a % 2 ^ n < 2 ^ n
Tactic:
apply Int.mod_lt Int.two_pow_pos
State after:
no goals