Theorem: Etch.Verification.Stream.IsStrictMono.lt' (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
H : toOrder s q ≤ i
hr : s.ready q = true
⊢ ↑(s.index q) < index' s (s.seek q i)
Tactic:
simpa using hs.lt H hr
State after:
no goals