proposition: Lemma diso_embedding (G H : sgraph) (g : plane_embedding G) (i : diso G H) : embedding (i \o g).
proof: Proof. case: g => D g [G1 G2 G3 G4] _ /= ; split => //=. - move=> x; have [d ? gd] := mapP (G2 (i^-1 x)). apply/mapP; exists d => //=. by rewrite -gd bijK'. - move=> d1 d2; by rewrite inj_eq. - move=> d1 d2; by rewrite edge_diso. 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)