Theorem: Relation.Preorder.co_irrefl (GMLInit/Logic/Ordering.lean)

State before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x : α
⊢ ¬coRel r x x
Tactic:
exact not_not_intro Reflexive.rfl
State after:
no goals