proposition: Lemma has_prim_root (F : fieldType) (n : nat) (rs : seq F) : n > 0 -> all n.-unity_root rs -> uniq rs -> size rs >= n -> has n.-primitive_root rs.
proof: Proof. move=> n_gt0 rsn1 Urs; rewrite leq_eqVlt ltnNge max_unity_roots // orbF eq_sym. move/eqP=> sz_rs; pose r := val (_ : seq_sub rs). have rn1 x: r x ^+ n = 1. by apply/eqP; rewrite -unity_rootE (allP rsn1) ?(valP x). have prim_r z: z ^+ n = 1 -> z \in rs. by move/eqP; rewrite -unity_rootE -(mem_unity_roots n_gt0). pose r' := SeqSub (prim_r _ _); pose sG_1 := r' _ (expr1n _ _). have sG_VP: r _ ^+ n.-1 ^+ n = 1. by move=> x; rewrite -exprM mulnC exprM rn1 expr1n. have sG_MP: (r _ * r _) ^+ n = 1 by move=> x y; rewrite exprMn !rn1 mul1r. pose sG_V := r' _ (sG_VP _); pose sG_M := r' _ (sG_MP _ _). have sG_Ag: associative sG_M by move=> x y z; apply: val_inj; rewrite /= mulrA. have sG_1g: left_id sG_1 sG_M by move=> x; apply: val_inj; rewrite /= mul1r. have sG_Vg: left_inverse sG_1 sG_V sG_M. by move=> x; apply: val_inj; rewrite /= -exprSr prednK ?rn1. exact: has_prim_root_subproof. 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)