fact: Structure mixin_of (T : eqType) := Mixin {ordering : rel T; _ : irreflexive ordering; _ : transitive ordering; _ : forall x y, x != y -> ordering x y || ordering y x}.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path fintype) pcm(options)