Theorem: Order.irrefl (QuickSortInLean/Order.lean)

State before:
α : Type
inst✝ : Order α
x : α
⊢ ¬x < x
Tactic:
simp [ltOfOrd, cmp_eq_of_eq]
State after:
no goals