proposition: Lemma index_finv (T : finType) (f : T -> T) x : findex f x (finv f x) = (order f x).-1.
proof: Proof. by rewrite findex_iter // orderSpred. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)