fact: Structure sorderb (M : Type) (R : M -> M -> bool) : Type := SOrderb { irreflsb : irreflexive R; transsb : transitive R } .
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)