proposition: Lemma emb_degree d : #|N(f d)| <= order node d.
proof: Proof. set x := f d. have Nxd z : z \in N(x) -> exists ez, cnode (emb_inv z) (edge ez) && cnode (emb_inv x) ez. { rewrite in_opn -{1}[x]emb_invK -{1}[z]emb_invK -emb_edge /adjn //. case/exists_inP => dz; rewrite !inE. exists dz; apply/andP => //. } pose h (z:G) := if @idP (z \in N(x)) is ReflectT zx then xchoose (Nxd _ zx) else d. have I : {in N(x)&, injective h}. { move => u v. rewrite /h. case: {1}_ / idP => // ux _. case: {1}_ / idP => // vx _. case: xchooseP' => du. case: xchooseP' => dv. move=> /andP [C1 _] /andP[C2 _] E; subst dv; apply/eqP. rewrite -[u]emb_invK -[v]emb_invK -emb_vertex //. by apply: connect_trans C2 _; rewrite cnodeC. } rewrite -(card_in_imset I). apply/subset_leq_card/subsetP => dz /imsetP [z xz ->] {dz}. rewrite /h; case: {-}_ / idP => [p|]; last by rewrite xz. case: xchooseP' => dz /andP [_ D2]. exact: connect_trans (emb_inv_node _) _. 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)