proposition: Lemma orbit_rot_iter n (inj_f : injective f) x o : orbit f x = o -> orbit f (iter n f x) = iter n (rot 1) o.
proof: Proof. by move <-; elim: n => // n IHn; rewrite !iterS -IHn orbit_rot1. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)