proposition: Proposition face_uniq (s : seq G) : 2.-connected G -> sface s -> uniq s.
proof: Proof. move => tcG; have := @two_connected_cyle (emb_map g). case/(_ _ _ _ _ )/Wrap; auto using plane_emb_plain, plane_emb_loopless. - exact/(two_connected_avoid_one (emb_embedding g)). - move=> Hg [x ->]; rewrite map_inj_in_uniq ?orbit_uniq //. move => u v; rewrite -!fconnect_orbit => Hu Hv. apply: contra_eq => uDv; rewrite -plane_emb_vertex. apply: Hg uDv _. apply: connect_trans Hv. by rewrite cfaceC. 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)