proposition: Lemma arcEmap (aT rT : eqType) (f : aT -> rT) (x y : aT) (p : seq aT) (s := [seq f x | x <- p]) : uniq s -> uniq p -> x != y -> x \in p -> y \in p -> arc s (f x) (f y) = [seq f x | x <- arc p x y].
proof: Proof. move=> uniq_s uniq_p xDy x_p y_p. have [i p1 p2 arc1 arc2 rot_i] := rot_to_arc uniq_p x_p y_p xDy. rewrite /s -(arc_rot i) ?map_f // -map_rot rot_i /= map_cat /= -arc1 left_arc //. by move: uniq_s; rewrite /s -(rot_uniq i) -map_rot rot_i /= map_cat. 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)