proposition: Lemma im_eltm : eltm dvd_y_x @* <[x]> = <[y]>.
proof: Proof. by rewrite morphim_cycle ?cycle_id //= eltm_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm automorphism quotient gproduct ssralg) mathcomp(finalg zmodp poly)