fact: Structure orderb (M : Type) (R : M -> M -> bool) : Type := Orderb { reflb : reflexive R; antisymb : antisymmetric R; transb : transitive R } .
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)