proposition: Lemma morphim_cycle x : x \in D -> f @* <[x]> = <[f x]>.
proof: Proof. by move=> Dx; rewrite morphim_gen (sub1set, morphim_set1). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)