proposition: Lemma exercise3_4a G: ( emptyset \cg G = emptyset /\ G \cg emptyset = emptyset).
proof: Proof. split; apply /set0_P => x /compg_P [_]. by move => [y _ /in_set0]. by move => [y /in_set0]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)