proposition: Lemma plane_emb_face x y : x -- y -> exists s, sface (x::y::s).
proof: Proof. have [dx /esym g_dx] := codomP (plane_emb_surj g x). have [dy /esym g_dy] := codomP (plane_emb_surj g y). rewrite -{1}g_dx -{1}g_dy -plane_emb_edge => /exists_inP [z]; rewrite !inE. rewrite plane_emb_vertex => /eqP dx_z dx_ez. set v := finv node (edge z). have fz : face z = v. { rewrite /v -plain_eq' ?finv_f //. exact: plane_emb_plain. } exists (drop 2 (map g (orbit face z))), z ; rewrite /sface. have X : 1 < arity z by apply plane_emb_arity2. rewrite [in RHS](orbit_prefix X) /= map_drop; congr (_ :: _ :: _). - by rewrite -g_dx. - by apply/eqP; rewrite -g_dy fz /v -plane_emb_vertex cnode1r f_finv. 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)