fact: Definition order_prod_r r g := fun x x' => forall j, least (induced_order r (Zo (domain g) (fun i => Vg x i <> Vg x' i))) j -> glt (Vg g j) (Vg x j)(Vg x' j).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)