proposition: Lemma rot_orbit (T : finType) (f : T -> T) x n (injf : injective f) : n < order f x -> rot n (orbit f x) = orbit f (iter n f x).
proof: Proof. move=> n_lt_ordx. rewrite [RHS](orbitE (cycle_orbit injf x)) -/(findex f _ _) ?findex_iter //. by rewrite -fconnect_orbit fconnect_iter. 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)