apply Int.add_ge_zero
case true
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 0 ≤ 2 ^ sz + toUint n'
case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 2 ^ sz ≥ 0

case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0