proposition: Lemma iter_order_cycle : {in p &, forall x y, iter (order x) f y = y}.
proof: Proof. by move=> x y xp yp; rewrite (eq_order_cycle yp) ?(iter_order_in homo_f f_inj). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)