proposition: Lemma iter_finv_in n : {in S, forall x, n <= order x -> iter n finv x = iter (order x - n) f x}.
proof: Proof. move=> x xS; rewrite -[x in LHS]iter_order_in => // /subnKC {1}<-. move: (_ - n) => m; rewrite iterD; elim: n => // n {2}<-. by rewrite iterSr /= finv_f_in // -iterD iter_in. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)