I've decided to follow this course in Coq, and it already hit me in the head, meaning I have still much more to learn after not being able to formalize preorders (on the inductive type level as I presumed possible).

Still, I made a promise, so I dug deep in Coq's standard library to find it's default implementation. Those are available here: https://github.com/vukovinski/azimuth-act/blob/master/chapter-1/poset.v

My next update should solve some puzzles by providing instances to the classes defined in the file above. I'll also write a short readme.md on how to work with Coq.