fact: Definition orthogonal_order r r' := forall x y, inc x (substrate r) -> inc y (substrate r) -> x <> y -> exactly_one (ocomparable r x y) (ocomparable r' x y).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)