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

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