fact: Structure mixin_of (T : eqType) := Mixin {ordering : rel T; _ : irreflexive ordering; _ : transitive ordering; _ : forall x y, [|| ordering x y, x == y | ordering y x]}.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq fintype)