Theorem: Etch.Verification.Stream.IsMonotonic.eq_zero_of_lt_index (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
i : ι
⊢ ↑i < index' s q → (eval s q) i = 0
Tactic:
contrapose!
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
i : ι
⊢ (eval s q) i ≠ 0 → index' s q ≤ ↑i

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
i : ι
⊢ (eval s q) i ≠ 0 → index' s q ≤ ↑i
Tactic:
exact hs.index_le_of_mem_support i
State after:
no goals