proposition: Lemma emb_gcomp x y : gcomp x y = connect (--) (f x) (f y).
proof: Proof. have ? : plain D by apply: emb_plain emb_f. rewrite -clink_glink; apply/idP/idP; move/connectP => [p]. - move=> pth_p ->; elim: p x pth_p => //= z p IHp x /andP [xz {}/IHp]. apply: connect_trans; have [/eqP<-|/eqP<-] := orP xz. + by apply/eq_connect0/eqP; rewrite -emb_vertex // cnode1r f_finv. + by apply: connect1; rewrite -emb_edge //= adjn_face. - move => pth_p lst_p; have q := Path_of_path pth_p; rewrite -lst_p in q. by have [r [pth_r lst_r _]] := emb_path_f q; apply/connectP; exists r. 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)