rw [add_sub_cancel] at h8
case h
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) ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)
case h
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 : z ≤ s (z - s 0).toNat
h6 : 0 ≤ z - s 0
h7 : ↑(z - s 0).toNat = z - s 0
⊢ z ≤ s ((z - s 0).toNat + 1)