proposition: Lemma olex_nFe_Ee: (substrate r' <> emptyset) -> (substrate r = emptyset) -> olexp_G = emptyset.
proof: Proof. move=> h1 h2; apply /set0_P => y /Zo_P [] /gfunctions_P1 [_ pa]. by rewrite h2 setX_0r => ye;case: h1;rewrite - pa; apply/domain_set0_P /sub_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)