proposition: Lemma iter_finv_cycle n : {in p, forall x, n <= order x -> iter n finv x = iter (order x - n) f x}.
proof: Proof. exact: iter_finv_in. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)