omega
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h5 : ∀ (i : ℕ), s 0 + ↑i ≤ s i
h8 : s 0 + ↑(z - s 0).toNat ≤ s (z - s 0).toNat
⊢ 0 ≤ z - s 0
no goals