proposition: Lemma bar (T : finType) (f : T -> T) x : injective f -> findex f (f x) x = (order f (f x)).-1.
proof: Proof. move => inj_f. have := index_finv f (f x). by rewrite finv_f. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)