cases' Nat.eq_zero_or_pos (Nat.find h3) with h5 h5
case h.refine_1
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
⊢ s (Nat.find h3) < z
case h.refine_1.inl
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 = 0
⊢ s (Nat.find h3) < z

case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
⊢ s (Nat.find h3) < z