@Filip #42 that is a really interesting experiment! I am no expert of coq, so what I say may be completely meaningless. But, could you use some of the typeclasses from the standard library for preorders, posets and ordered sets? I think the definition of preorder there is very close to the one you give in your file. Maybe staying close to the standard library can help to smooth some of the obstacles