proposition: Lemma rot_face n (s : seq G) : sface s -> sface (rot n s).
proof: Proof. have [n_lt_s face_s|?] := ltnP n (size s); last by rewrite rot_oversize. case: face_s n n_lt_s => x -> n; rewrite size_map size_orbit => n_lt_o. rewrite -map_rot rot_orbit; [by eexists|exact: faceI|done]. 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)