fact: Definition are_preorder_inv (f : A -> B) (g : B -> A) := (@is_preorder_morph A B rA rB f) /\ (@is_preorder_morph B A rB rA g) /\ (are_inv f g).
imports: Coq(Relation_Definitions Morphisms) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Mon(SPropBase) mathcomp(all_ssreflect boolp)