proposition: Lemma hiso_embed (E : hypermap) (i : hiso E D) : embedding f -> embedding (f \o i).
proof: Proof. case => E1 E2 E3 E4. split. - by rewrite (hiso_plain i). - move => x; case/mapP : (E2 x) => x0 _ ->. by rewrite -[x0](bijK' i) codom_f. - move => x y /=. by rewrite (hiso_cnode i). - move => x y /=. by rewrite -E4 hiso_adjn. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)