intro cxy cyz rzx
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
x y z : α
⊢ coRel r x y → coRel r y z → coRel r x z
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
x y z : α
cxy : coRel r x y
cyz : coRel r y z
rzx : r z x
⊢ False