fact: Definition order_morphism d (T : porderType d) d' (T' : porderType d') (f : T -> T') : Prop := {mono f : x y / x <= y}.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)