proposition: Lemma embedding_g' : embedding g'.
proof: Proof. have n_dxy : ~~ @cnode[D] dx dy. by rewrite plane_emb_vertex g_dx g_dy. have llD : loopless D by apply plane_emb_loopless. have nAdydy : ~~ @adjn[D] dx dy by rewrite plane_emb_edge g_dx g_dy xNy. have llD' : loopless D' by apply merge_loopless. have subDD' : subrel @cnode[D] @cnode[D'] by apply: switch_subrel. have adjnD' (d1 d2 : D) : g d1 = y -> @adjn[D'] d1 d2 = @adjn[D] d2 dx || @adjn[D] d2 dy. { move => g1_y. apply: adjn_merge1 => //. by rewrite (plane_emb_vertex) g_dy g1_y. } have adjnD'' (d1 d2 : D) : g d1 = x -> @adjn[D'] d1 d2 = @adjn[D] d2 dx || @adjn[D] d2 dy. { move => g1_y. rewrite /D' adjn_mergeC orbC. apply: adjn_merge1 => //; first by rewrite eq_sym. by rewrite cnodeC. by rewrite adjnC. by rewrite (plane_emb_vertex) g_dx g1_y. } split => //. - case => z zDy. have [z0 g_z0] := codomP (plane_emb_surj g z). by apply/codomP; exists z0; apply: val_inj; rewrite /g'/= -g_z0 altF. - move => d1 d2; rewrite cnode_merge // !plane_emb_vertex /g'. case: {-}_ / boolP => [/eqP g1_y|g1Dy]; case: {-}_ / boolP => [/eqP g2_y|g2Dy]. all: rewrite -val_eqE /= ?g1_y ?g2_y ?g_dx ?g_dy ?eqxx //. all: by rewrite ?[y == _]eq_sym ?[_ == x]eq_sym ?(negbTE xDy) ?(negbTE g2Dy) ?(negbTE g1Dy). - move => d1 d2. rewrite /g'. case: {-}_ / boolP => [/eqP g1_y|g1Dy]; case: {-}_ / boolP => [/eqP g2_y|g2Dy]. + rewrite sgP. have n12 : @cnode[D] d1 d2 by rewrite (plane_emb_vertex) g1_y g2_y. apply: contraNF llD' => /exists_inP [z]; rewrite !inE => A1 A2. rewrite cnodeC in A1. apply/existsP; exists z. apply: connect_trans A2. apply: connect_trans A1 _. by apply: switch_subrel n12. + rewrite adjnD' //. rewrite /edge_rel/= eqxx andbF /= !plane_emb_edge g_dx g_dy. case: (eqVneq (g d2) x) => //= ->. by rewrite sgP. + rewrite adjnC // adjnD' // !plane_emb_edge g_dx g_dy [RHS]/edge_rel/= !eqxx andbF /=. case: (eqVneq (g d1) x) => //= ->. by rewrite sgP. + rewrite /edge_rel/=. have [|] := boolP ((g d1 == x) || (g d2 == x)). * case: (eqVneq (g d1) x) => [g1x|g1Dx]; case: (eqVneq (g d2) x) => [g2x|g2Dx] => //= _. -- rewrite g1x g2x sgP adjn_loopless //. apply: subDD'. by rewrite plane_emb_vertex g1x g2x. -- by rewrite adjnD'' // !plane_emb_edge g_dx g_dy. -- by rewrite adjnC // adjnD'' // !plane_emb_edge g_dx g_dy. * rewrite negb_or => /andP[g1Dx g2Dx]; rewrite (negbTE g1Dx) (negbTE g2Dx) /=. by rewrite adjn_merge2 // ?(plane_emb_vertex) ?g_dx ?g_dy // plane_emb_edge. 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)