proposition: Lemma Aut_prime_cycle_cyclic (a : gT) : prime #[a] -> cyclic (Aut <[a]>).
proof: Proof. move=> pr_a; have inj_um := injm_Zp_unitm a. have /eq_S/eq_S eq_a := Fp_Zcast pr_a. pose fm := cast_ord (esym eq_a) \o val \o invm inj_um. apply: (@field_mul_group_cyclic _ _ _ fm) => [f g Af Ag | f Af] /=. by apply: val_inj; rewrite /= morphM ?im_Zp_unitm //= eq_a. split=> [/= fm1 |->]; last by apply: val_inj; rewrite /= morph1. apply: (injm1 (injm_invm inj_um)); first by rewrite /= im_Zp_unitm. by do 2!apply: val_inj; move/(congr1 val): fm1. 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)