Theorem: Etch.Verification.fst_lt_of_lt_of_lt (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type ?u.114137
inst✝¹ : LinearOrder ι
α : Type u_1
inst✝ : Preorder α
x y : Lex (α × Bool)
z : α
h₁ : x < y
h₂ : y < (z, false)
⊢ (z, false).2 ≤ x.2
Tactic:
simp
State after:
no goals

State before:
ι : Type ?u.114137
inst✝¹ : LinearOrder ι
α : Type u_1
inst✝ : Preorder α
x : Lex (α × Bool)
y z : α
h₁ : x < (y, true)
h₂ : (y, true) < (z, true)
⊢ y < (z, true).1
Tactic:
simpa using h₂
State after:
no goals

State before:
ι : Type ?u.114137
inst✝¹ : LinearOrder ι
α : Type u_1
inst✝ : Preorder α
x : Lex (α × Bool)
y z : α
h₁ : x < (y, false)
h₂ : (y, false) < (z, true)
⊢ (y, false).2 ≤ x.2
Tactic:
simp
State after:
no goals