rw [coRel_iff_asymRel]
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y z : α
⊢ asymRel r x y → asymRel r y z → coRel r x z
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y z : α
⊢ asymRel r x y → asymRel r y z → asymRel r x z