proposition: Lemma order_max (T : finType) (f : T -> T) (x : T) : order f x <= #|T|.
proof: Proof. by rewrite -size_orbit -(card_uniqP _) ?max_card ?orbit_uniq. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)