Theorem: Prod.Lex.lt_mk_true_iff (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β : Type ?u.53384
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝ : PartialOrder α
x : Lex (α × Bool)
y : α
⊢ x < (y, true) ↔ x ≤ (y, false)
Tactic:
simp [lt_iff', le_iff']
State after:
no goals