proposition: Lemma iter_order_in : {in S, forall x, iter (order x) f x = x}.
proof: Proof. by move=> x xS; rewrite -orderSpred iterS; apply: f_finv_in. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)