proposition: Lemma del_vertex_emb_embedding : embedding del_vertex_emb.
proof: Proof. have [plainD surj_g vertex_g edge_g] := emb_embedding g. rewrite -/D in plainD vertex_g edge_g. split. - exact/del_node_plain. - move => y. have [y0 g_y0] := codomP (surj_g (val y)); apply/codomP. have Hy : ~~ cnode d y0. by apply: contraTN (valP y); rewrite !inE negbK cnodeC vertex_g -g_y0 emb_invK. have [/del_node_neighbor1|y0N]:= boolP (y0 \in N). + case/(_ _ _ _ _)/Wrap => // ny0N. exists (Sub (node y0) ny0N). by apply: val_inj; rewrite /= g_y0; apply/eqP; rewrite -vertex_g -cnode1r. + by exists (Sub y0 y0N); exact: val_inj. - by move=> d1 d2; rewrite del_node_cnode vertex_g /del_vertex_emb -val_eqE. - by move=> d1 d2; rewrite del_node_adjn // edge_g /del_vertex_emb. 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)