proposition: Lemma orbit_case (T : finType) (f : T -> T) (x : T) : exists o, orbit f x = x :: o.
proof: Proof. by rewrite /orbit -orderSpred /=; eexists. 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)