Theorem: max_ne_self_iff' (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
⊢ ¬b = max a b ↔ b < a
Tactic:
rw [max_comm]
State after:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
⊢ ¬b = max b a ↔ b < a

State before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
⊢ ¬b = max b a ↔ b < a
Tactic:
simp
State after:
no goals