proposition: Lemma ker_eltm : 'ker (eltm dvd_y_x) = <[x ^+ #[y]]>.
proof: Proof. apply/eqP; rewrite eq_sym eqEcard cycle_subG 3!inE mem_cycle /= eltmE. rewrite expg_order eqxx (orderE y) -im_eltm card_morphim setIid -orderE. by rewrite orderXdiv ?dvdn_indexg //= leq_divRL ?indexg_gt0 ?Lagrange ?subsetIl. 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)