proposition: Lemma oprod_zero r g: (exists2 i, inc i (domain g) & substrate (Vg g i) = emptyset) -> order_prod r g = emptyset.
proof: Proof. move=> [j jdg Vz]. apply /set0_P => q /Zo_P [] /setX_P [_ /setXf_P [fgy dy p]]. by move: (p _ jdg); rewrite Vz => /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)