proposition: Lemma codom_gcompd : codom gcompd =i gcomp z.
proof: Proof. by move=> x; apply/imageP/idP => [[[y zGy] _ -> //] | zGx]; exists (sub x zGx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)