case next sz bn n' ih =>
  cases bn <;> simp [@ih n']
  apply Int.add_ge_zero; apply Int.pow_ge_zero; decide; apply ih
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 0 ≤ toUint (next bn n')
no goals