proposition: Lemma eltmE i : eltm dvd_y_x (x ^+ i) = y ^+ i.
proof: Proof. apply/eqP; rewrite eq_expg_mod_order. have [x_le1 | x_gt1] := leqP #[x] 1. suffices: #[y] %| 1 by rewrite dvdn1 => /eqP->; rewrite !modn1. by rewrite (dvdn_trans dvd_y_x) // dvdn1 order_eq1 -cycle_eq1 trivg_card_le1. rewrite -(expg_znat i (cycle_id x)) invmE /=; last by rewrite /Zp x_gt1 inE. by rewrite val_Zp_nat // modn_dvdm. 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)