proposition: Lemma plane_add_node1 (G : sgraph) (g : plane_embedding G) (x : G) s : sface g (x::s) -> exists g' : plane_embedding (add_node G [set x]), sface g' [:: Some x, None, Some x & map Some s].
proof: Proof. pose D := emb_map g. case => z forbit_z. set G' := add_node G [set x]. pose D' := h_add_node z. pose g' (z' : D') : G' := match z' with | IcpX => Some (g z) | IcpXe => None | Icp z' => Some (g z') end. have gz : g z = x. { by move: forbit_z; rewrite /orbit -orderSpred /=; case=> -> _. } have [plain_D surj_g vertex_g edge_g] := emb_embedding g. have plain_D' := add_node_plain z plain_D : plain D'. have embedding_g' : embedding g'. { split. - by apply: add_node_plain (plane_emb_plain _). - move => [u|]; last by apply/codomP; exists IcpXe. by have [d _ ->] := mapP (surj_g u); apply/codomP; exists (Icp d). - have ? := @nodeI D'. move => [||d1] [||d2]; rewrite /= ?connect0 ?eqxx //=. all: rewrite ?[_ _ IcpXe](@cnodeC D') ?add_node_cnodeXe //. all: rewrite ?[_ _ IcpX](@cnodeC D') ?Some_eqE ?[_ IcpX _]same_fconnect1 //=. all: rewrite ?(@add_node_cnodeE) -?cnode1 // 1?cnodeC //. - have adjn_Icp := @add_node_adjn D z. pose m (d : D') := match d with IcpX => 1 | IcpXe => 2 | _ => 0 end. move => d1 d2; wlog: d1 d2 / m d1 <= m d2 => [W|]. { have [|/ltnW] := leqP (m d1) (m d2); first exact: W. rewrite sg_sym adjnC //. exact: W. } move: d1 d2 => [||d1] [||d2] // _ ; rewrite /= ?sg_irrefl. all: rewrite /edge_rel/= ?inE ?eqxx ?[in g z == x]gz ?eqxx. + by rewrite adjn_node1 adjn_node1r /= adjn_Icp edge_g sg_irrefl. + exact: adjn_edge. + exact: add_node_adjnXeXe. + by rewrite adjn_node1r /= adjn_Icp -adjn_node1r. + by rewrite -gz -vertex_g adjnC // add_node_adjnXe cnodeC. + by rewrite adjn_Icp. } have planar_D' : planar D' by rewrite add_node_planar; apply: emb_planar. exists (Build_plane_embedding embedding_g' planar_D'). exists (IcpX) => /=. rewrite add_node_face_orbitE /= gz -map_cons forbit_z; congr ([:: _ , _ & _]). by rewrite -!map_comp; apply: eq_map. 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)