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

State before:
sz : ℕ
b : Bool
n : FinInt sz
⊢ toUint (next b n) < 2 ^ sz ↔ b = false
Tactic:
sorry
State after:
no goals