packaging fingroup and algebra

The files zmodp and cyclic in fingroup had dependecies in algebra so I put them there.
I'm not convinced it's the best solution to this problem.
Maybe more subdivisions in algebra would bring a better solution?

(Maybe we should send the whole problem to a solver? :P)

10 files changed, 1297 insertions, 10 deletions

diff --git a/mathcomp/algebra/AUTHORS b/mathcomp/algebra/AUTHORS
new file mode 120000
index 0000000..b55a98d
--- /dev/null
+++ b/mathcomp/algebra/AUTHORS
@@ -0,0 +1 @@
+../../etc/AUTHORS
\ No newline at end of file
diff --git a/mathcomp/algebra/CeCILL-B b/mathcomp/algebra/CeCILL-B
new file mode 120000
index 0000000..83e22fd
--- /dev/null
+++ b/mathcomp/algebra/CeCILL-B
@@ -0,0 +1 @@
+../../etc/CeCILL-B
\ No newline at end of file
diff --git a/mathcomp/algebra/INSTALL b/mathcomp/algebra/INSTALL
new file mode 120000
index 0000000..6aa7ec5
--- /dev/null
+++ b/mathcomp/algebra/INSTALL
@@ -0,0 +1 @@
+../../etc/INSTALL
\ No newline at end of file
diff --git a/mathcomp/algebra/Make b/mathcomp/algebra/Make
new file mode 100644
index 0000000..d9f4c63
--- /dev/null
+++ b/mathcomp/algebra/Make
@@ -0,0 +1,21 @@
+all.v
+finalg.v
+fraction.v
+intdiv.v
+interval.v
+matrix.v
+mxalgebra.v
+mxpoly.v
+polydiv.v
+poly.v
+polyXY.v
+rat.v
+ring_quotient.v
+ssralg.v
+ssrint.v
+ssrnum.v
+vector.v
+zmodp.v
+cyclic.v
+
+-R . mathcomp.algebra
diff --git a/mathcomp/algebra/Makefile b/mathcomp/algebra/Makefile
new file mode 100644
index 0000000..d693257
--- /dev/null
+++ b/mathcomp/algebra/Makefile
@@ -0,0 +1,23 @@
+H=@
+
+ifeq "$(COQBIN)" ""
+COQBIN=$(dir $(shell which coqtop))/
+endif
+
+
+OLD_MAKEFLAGS:=$(MAKEFLAGS)
+MAKEFLAGS+=-B
+
+.DEFAULT_GOAL := all
+
+%:
+	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
+	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+		-f Makefile.coq $*
+
+.PHONY: clean
+clean:
+	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+		-f Makefile.coq clean
+	$(H)rm -f Makefile.coq
+
diff --git a/mathcomp/algebra/README b/mathcomp/algebra/README
new file mode 120000
index 0000000..e4e30e8
--- /dev/null
+++ b/mathcomp/algebra/README
@@ -0,0 +1 @@
+../../etc/README
\ No newline at end of file
diff --git a/mathcomp/algebra/all.v b/mathcomp/algebra/all.v
index f4406a9..8a93ca9 100644
--- a/mathcomp/algebra/all.v
+++ b/mathcomp/algebra/all.v
@@ -1,16 +1,16 @@
+Require Export ssralg.
+Require Export ssrnum.
 Require Export finalg.
-Require Export fraction.
+Require Export poly.
+Require Export polydiv.
+Require Export polyXY.
+Require Export ssrint.
+Require Export rat.
 Require Export intdiv.
 Require Export interval.
 Require Export matrix.
-Require Export mxalgebra.
 Require Export mxpoly.
-Require Export polydiv.
-Require Export poly.
-Require Export polyXY.
-Require Export rat.
-Require Export ring_quotient.
-Require Export ssralg.
-Require Export ssrint.
-Require Export ssrnum.
+Require Export mxalgebra.
 Require Export vector.
+Require Export ring_quotient.
+Require Export fraction.
diff --git a/mathcomp/algebra/cyclic.v b/mathcomp/algebra/cyclic.v
new file mode 100644
index 0000000..ad10492
--- /dev/null
+++ b/mathcomp/algebra/cyclic.v
@@ -0,0 +1,865 @@
+(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype bigop.
+Require Import prime finset fingroup morphism perm automorphism quotient.
+Require Import gproduct ssralg finalg zmodp poly.
+
+(******************************************************************************)
+(*  Properties of cyclic groups.                                              *)
+(* Definitions:                                                               *)
+(* Defined in fingroup.v:                                                     *)
+(*           <[x]> == the cycle (cyclic group) generated by x.                *)
+(*            #[x] == the order of x, i.e., the cardinal of <[x]>.            *)
+(* Defined in prime.v:                                                        *)
+(*       totient n == Euler's totient function                                *)
+(* Definitions in this file:                                                  *)
+(*        cyclic G <=> G is a cyclic group.                                   *)
+(*    metacyclic G <=> G is a metacyclic group (i.e., a cyclic extension of a *)
+(*                     cyclic group).                                         *)
+(*   generator G x <=> x is a generator of the (cyclic) group G.              *)
+(*           Zpm x == the isomorphism mapping the additive group of integers  *)
+(*                    mod #[x] to the cyclic group <[x]>.                     *)
+(*      cyclem x n == the endomorphism y |-> y ^+ n of <[x]>.                 *)
+(*      Zp_unitm x == the isomorphism mapping the multiplicative group of the *)
+(*                    units of the ring of integers mod #[x] to the group of  *)
+(*                    automorphisms of <[x]> (i.e., Aut <[x]>).               *)
+(*                    Zp_unitm x maps u to cyclem x u.                        *)
+(*    eltm dvd_y_x == the smallest morphism (with domain <[x]>) mapping x to  *)
+(*                    y, given a proof dvd_y_x : #[y] %| #[x].                *)
+(*   expg_invn G k == if coprime #|G| k, the inverse of exponent k in G.      *)
+(* Basic results for these notions, plus the classical result that any finite *)
+(* group isomorphic to a subgroup of a field is cyclic, hence that Aut G is   *)
+(* cyclic when G is of prime order.                                           *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import GroupScope GRing.Theory.
+
+(***********************************************************************)
+(*  Cyclic groups.                                                     *)
+(***********************************************************************)
+
+Section Cyclic.
+
+Variable gT : finGroupType.
+Implicit Types (a x y : gT) (A B : {set gT}) (G K H : {group gT}).
+
+Definition cyclic A := [exists x, A == <[x]>].
+
+Lemma cyclicP A : reflect (exists x, A = <[x]>) (cyclic A).
+Proof. exact: exists_eqP. Qed.
+
+Lemma cycle_cyclic x : cyclic <[x]>.
+Proof. by apply/cyclicP; exists x. Qed.
+
+Lemma cyclic1 : cyclic [1 gT].
+Proof. by rewrite -cycle1 cycle_cyclic. Qed.
+
+(***********************************************************************)
+(* Isomorphism with the additive group                                 *)
+(***********************************************************************)
+
+Section Zpm.
+
+Variable a : gT.
+
+Definition Zpm (i : 'Z_#[a]) := a ^+ i.
+
+Lemma ZpmM : {in Zp #[a] &, {morph Zpm : x y / x * y}}.
+Proof.
+rewrite /Zpm; case: (eqVneq a 1) => [-> | nta] i j _ _.
+  by rewrite !expg1n ?mulg1.
+by rewrite /= {3}Zp_cast ?order_gt1 // expg_mod_order expgD.
+Qed.
+
+Canonical Zpm_morphism := Morphism ZpmM.
+
+Lemma im_Zpm : Zpm @* Zp #[a] = <[a]>.
+Proof.
+apply/eqP; rewrite eq_sym eqEcard cycle_subG /= andbC morphimEdom.
+rewrite (leq_trans (leq_imset_card _ _)) ?card_Zp //= /Zp order_gt1.
+case: eqP => /= [a1 | _]; first by rewrite imset_set1 morph1 a1 set11.
+by apply/imsetP; exists 1%R; rewrite ?expg1 ?inE.
+Qed.
+
+Lemma injm_Zpm : 'injm Zpm.
+Proof.
+apply/injmP/dinjectiveP/card_uniqP.
+rewrite size_map -cardE card_Zp //= {7}/order -im_Zpm morphimEdom /=.
+by apply: eq_card => x; apply/imageP/imsetP=> [] [i Zp_i ->]; exists i.
+Qed.
+
+Lemma eq_expg_mod_order m n : (a ^+ m == a ^+ n) = (m == n %[mod #[a]]).
+Proof.
+have [->|] := eqVneq a 1; first by rewrite order1 !modn1 !expg1n eqxx.
+rewrite -order_gt1 => lt1a; have ZpT: Zp #[a] = setT by rewrite /Zp lt1a.
+have: injective Zpm by move=> i j; apply (injmP injm_Zpm); rewrite /= ZpT inE.
+move/inj_eq=> eqZ; symmetry; rewrite -(Zp_cast lt1a).
+by rewrite -[_ == _](eqZ (inZp m) (inZp n)) /Zpm /= Zp_cast ?expg_mod_order.
+Qed.
+
+Lemma Zp_isom : isom (Zp #[a]) <[a]> Zpm.
+Proof. by apply/isomP; rewrite injm_Zpm im_Zpm. Qed.
+
+Lemma Zp_isog : isog (Zp #[a]) <[a]>.
+Proof. exact: isom_isog Zp_isom. Qed.
+
+End Zpm.
+
+(***********************************************************************)
+(*        Central and direct product of cycles                         *)
+(***********************************************************************)
+
+Lemma cyclic_abelian A : cyclic A -> abelian A.
+Proof. by case/cyclicP=> a ->; exact: cycle_abelian. Qed.
+
+Lemma cycleMsub a b :
+  commute a b -> coprime #[a] #[b] -> <[a]> \subset <[a * b]>.
+Proof.
+move=> cab co_ab; apply/subsetP=> _ /cycleP[k ->].
+apply/cycleP; exists (chinese #[a] #[b] k 0); symmetry.
+rewrite expgMn // -expg_mod_order chinese_modl // expg_mod_order.
+by rewrite /chinese addn0 -mulnA mulnCA expgM expg_order expg1n mulg1.
+Qed.
+
+Lemma cycleM a b :
+  commute a b -> coprime #[a] #[b] -> <[a * b]> = <[a]> * <[b]>.
+Proof.
+move=> cab co_ab; apply/eqP; rewrite eqEsubset -(cent_joinEl (cents_cycle cab)).
+rewrite join_subG {3}cab !cycleMsub // 1?coprime_sym //.
+by rewrite -genM_join cycle_subG mem_gen // mem_imset2 ?cycle_id.
+Qed.
+
+Lemma cyclicM A B :
+    cyclic A -> cyclic B -> B \subset 'C(A) -> coprime #|A| #|B| ->
+  cyclic (A * B).
+Proof.
+move=> /cyclicP[a ->] /cyclicP[b ->]; rewrite cent_cycle cycle_subG => cab coab.
+by rewrite -cycleM ?cycle_cyclic //; exact/esym/cent1P.
+Qed.
+
+Lemma cyclicY K H :
+    cyclic K -> cyclic H -> H \subset 'C(K) -> coprime #|K| #|H| ->
+  cyclic (K <*> H).
+Proof. by move=> cycK cycH cKH coKH; rewrite cent_joinEr // cyclicM. Qed.
+
+(***********************************************************************)
+(*        Order properties                                             *)
+(***********************************************************************)
+
+Lemma order_dvdn a n : #[a] %| n = (a ^+ n == 1).
+Proof. by rewrite (eq_expg_mod_order a n 0) mod0n. Qed.
+
+Lemma order_inf a n : a ^+ n.+1 == 1 -> #[a] <= n.+1.
+Proof. by rewrite -order_dvdn; exact: dvdn_leq. Qed.
+
+Lemma order_dvdG G a : a \in G -> #[a] %| #|G|.
+Proof. by move=> Ga; apply: cardSg; rewrite cycle_subG. Qed.
+
+Lemma expg_cardG G a : a \in G -> a ^+ #|G| = 1.
+Proof. by move=> Ga; apply/eqP; rewrite -order_dvdn order_dvdG. Qed.
+
+Lemma expg_znat G x k : x \in G -> x ^+ (k%:R : 'Z_(#|G|))%R = x ^+ k.
+Proof.
+case: (eqsVneq G 1) => [-> /set1P-> | ntG Gx]; first by rewrite !expg1n.
+apply/eqP; rewrite val_Zp_nat ?cardG_gt1 // eq_expg_mod_order.
+by rewrite modn_dvdm ?order_dvdG.
+Qed.
+
+Lemma expg_zneg G x (k : 'Z_(#|G|)) : x \in G -> x ^+ (- k)%R = x ^- k.
+Proof.
+move=> Gx; apply/eqP; rewrite eq_sym eq_invg_mul -expgD.
+by rewrite -(expg_znat _ Gx) natrD natr_Zp natr_negZp subrr.
+Qed.
+
+Lemma nt_gen_prime G x : prime #|G| -> x \in G^# -> G :=: <[x]>.
+Proof.
+move=> Gpr /setD1P[]; rewrite -cycle_subG -cycle_eq1 => ntX sXG.
+apply/eqP; rewrite eqEsubset sXG andbT.
+by apply: contraR ntX => /(prime_TIg Gpr); rewrite (setIidPr sXG) => ->.
+Qed.
+
+Lemma nt_prime_order p x : prime p -> x ^+ p = 1 -> x != 1 -> #[x] = p.
+Proof.
+move=> p_pr xp ntx; apply/prime_nt_dvdP; rewrite ?order_eq1 //.
+by rewrite order_dvdn xp.
+Qed.
+
+Lemma orderXdvd a n : #[a ^+ n] %| #[a].
+Proof. by apply: order_dvdG; exact: mem_cycle. Qed.
+
+Lemma orderXgcd a n : #[a ^+ n] = #[a] %/ gcdn #[a] n.
+Proof.
+apply/eqP; rewrite eqn_dvd; apply/andP; split.
+  rewrite order_dvdn -expgM -muln_divCA_gcd //.
+  by rewrite expgM expg_order expg1n.
+have [-> | n_gt0] := posnP n; first by rewrite gcdn0 divnn order_gt0 dvd1n.
+rewrite -(dvdn_pmul2r n_gt0) divn_mulAC ?dvdn_gcdl // dvdn_lcm.
+by rewrite order_dvdn mulnC expgM expg_order eqxx dvdn_mulr.
+Qed.
+
+Lemma orderXdiv a n : n %| #[a] -> #[a ^+ n] = #[a] %/ n.
+Proof. by case/dvdnP=> q defq; rewrite orderXgcd {2}defq gcdnC gcdnMl. Qed.
+
+Lemma orderXexp p m n x : #[x] = (p ^ n)%N -> #[x ^+ (p ^ m)] = (p ^ (n - m))%N.
+Proof.
+move=> ox; have [n_le_m | m_lt_n] := leqP n m.
+  rewrite -(subnKC n_le_m) subnDA subnn expnD expgM -ox.
+  by rewrite expg_order expg1n order1.
+rewrite orderXdiv ox ?dvdn_exp2l ?expnB ?(ltnW m_lt_n) //.
+by have:= order_gt0 x; rewrite ox expn_gt0 orbC -(ltn_predK m_lt_n).
+Qed.
+
+Lemma orderXpfactor p k n x :
+  #[x ^+ (p ^ k)] = n -> prime p -> p %| n -> #[x] = (p ^ k * n)%N.
+Proof.
+move=> oxp p_pr dv_p_n.
+suffices pk_x: p ^ k %| #[x] by rewrite -oxp orderXdiv // mulnC divnK.
+rewrite pfactor_dvdn // leqNgt; apply: contraL dv_p_n => lt_x_k.
+rewrite -oxp -p'natE // -(subnKC (ltnW lt_x_k)) expnD expgM.
+rewrite (pnat_dvd (orderXdvd _ _)) // -p_part // orderXdiv ?dvdn_part //.
+by rewrite -{1}[#[x]](partnC p) // mulKn // part_pnat.
+Qed.
+
+Lemma orderXprime p n x :
+  #[x ^+ p] = n -> prime p -> p %| n -> #[x] = (p * n)%N.
+Proof. exact: (@orderXpfactor p 1). Qed.
+
+Lemma orderXpnat m n x : #[x ^+ m] = n -> \pi(n).-nat m -> #[x] = (m * n)%N.
+Proof.
+move=> oxm n_m; have [m_gt0 _] := andP n_m.
+suffices m_x: m %| #[x] by rewrite -oxm orderXdiv // mulnC divnK.
+apply/dvdn_partP=> // p; rewrite mem_primes => /and3P[p_pr _ p_m].
+have n_p: p \in \pi(n) by apply: (pnatP _ _ n_m).
+have p_oxm: p %| #[x ^+ (p ^ logn p m)].
+  apply: dvdn_trans (orderXdvd _ m`_p^'); rewrite -expgM -p_part ?partnC //.
+  by rewrite oxm; rewrite mem_primes in n_p; case/and3P: n_p.
+by rewrite (orderXpfactor (erefl _) p_pr p_oxm) p_part // dvdn_mulr.
+Qed.
+
+Lemma orderM a b :
+  commute a b -> coprime #[a] #[b] -> #[a * b] = (#[a] * #[b])%N.
+Proof. by move=> cab co_ab; rewrite -coprime_cardMg -?cycleM. Qed.
+
+Definition expg_invn A k := (egcdn k #|A|).1.
+
+Lemma expgK G k :
+  coprime #|G| k -> {in G, cancel (expgn^~ k) (expgn^~ (expg_invn G k))}.
+Proof.
+move=> coGk x /order_dvdG Gx; apply/eqP.
+rewrite -expgM (eq_expg_mod_order _ _ 1) -(modn_dvdm 1 Gx).
+by rewrite -(chinese_modl coGk 1 0) /chinese mul1n addn0 modn_dvdm.
+Qed.
+
+Lemma cyclic_dprod K H G :
+  K \x H = G -> cyclic K -> cyclic H -> cyclic G = coprime #|K| #|H| .
+Proof.
+case/dprodP=> _ defKH cKH tiKH cycK cycH; pose m := lcmn #|K| #|H|.
+apply/idP/idP=> [/cyclicP[x defG] | coKH]; last by rewrite -defKH cyclicM.
+rewrite /coprime -dvdn1 -(@dvdn_pmul2l m) ?lcmn_gt0 ?cardG_gt0 //.
+rewrite muln_lcm_gcd muln1 -TI_cardMg // defKH defG order_dvdn.
+have /mulsgP[y z Ky Hz ->]: x \in K * H by rewrite defKH defG cycle_id.
+rewrite -[1]mulg1 expgMn; last exact/commute_sym/(centsP cKH).
+apply/eqP; congr (_ * _); apply/eqP; rewrite -order_dvdn.
+  exact: dvdn_trans (order_dvdG Ky) (dvdn_lcml _ _).
+exact: dvdn_trans (order_dvdG Hz) (dvdn_lcmr _ _).
+Qed.
+
+(***********************************************************************)
+(*        Generator                                                    *)
+(***********************************************************************)
+
+Definition generator (A : {set gT}) a := A == <[a]>.
+
+Lemma generator_cycle a : generator <[a]> a.
+Proof. exact: eqxx. Qed.
+
+Lemma cycle_generator a x : generator <[a]> x -> x \in <[a]>.
+Proof. by move/(<[a]> =P _)->; exact: cycle_id. Qed.
+
+Lemma generator_order a b : generator <[a]> b -> #[a] = #[b].
+Proof. by rewrite /order => /(<[a]> =P _)->. Qed.
+
+End Cyclic.
+
+Arguments Scope cyclic [_ group_scope].
+Arguments Scope generator [_ group_scope group_scope].
+Arguments Scope expg_invn [_ group_scope nat_scope].
+Implicit Arguments cyclicP [gT A].
+Prenex Implicits cyclic Zpm generator expg_invn.
+
+(* Euler's theorem *)
+Theorem Euler_exp_totient a n : coprime a n -> a ^ totient n  = 1 %[mod n].
+Proof.
+case: n => [|[|n']] //; [by rewrite !modn1 | set n := n'.+2] => co_a_n.
+have{co_a_n} Ua: coprime n (inZp a : 'I_n) by rewrite coprime_sym coprime_modl.
+have: FinRing.unit 'Z_n Ua ^+ totient n == 1.
+  by rewrite -card_units_Zp // -order_dvdn order_dvdG ?inE.
+by rewrite -2!val_eqE unit_Zp_expg /= -/n modnXm => /eqP.
+Qed.
+
+Section Eltm.
+
+Variables (aT rT : finGroupType) (x : aT) (y : rT).
+
+Definition eltm of #[y] %| #[x] := fun x_i => y ^+ invm (injm_Zpm x) x_i.
+
+Hypothesis dvd_y_x : #[y] %| #[x].
+
+Lemma eltmE i : eltm dvd_y_x (x ^+ i) = y ^+ i.
+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.
+
+Lemma eltm_id : eltm dvd_y_x x = y. Proof. exact: (eltmE 1). Qed.
+
+Lemma eltmM : {in <[x]> &, {morph eltm dvd_y_x : x_i x_j / x_i * x_j}}.
+Proof.
+move=> _ _ /cycleP[i ->] /cycleP[j ->].
+by apply/eqP; rewrite -expgD !eltmE expgD.
+Qed.
+Canonical eltm_morphism := Morphism eltmM.
+
+Lemma im_eltm : eltm dvd_y_x @* <[x]> = <[y]>.
+Proof. by rewrite morphim_cycle ?cycle_id //= eltm_id. Qed.
+
+Lemma ker_eltm : 'ker (eltm dvd_y_x) = <[x ^+ #[y]]>.
+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.
+
+Lemma injm_eltm : 'injm (eltm dvd_y_x) = (#[x] %| #[y]).
+Proof. by rewrite ker_eltm subG1 cycle_eq1 -order_dvdn. Qed.
+
+End Eltm.
+
+Section CycleSubGroup.
+
+Variable gT : finGroupType.
+
+(*  Gorenstein, 1.3.1 (i) *)
+Lemma cycle_sub_group (a : gT) m :
+     m %| #[a] ->
+  [set H : {group gT} | H \subset <[a]> & #|H| == m]
+     = [set <[a ^+ (#[a] %/ m)]>%G].
+Proof.
+move=> m_dv_a; have m_gt0: 0 < m by apply: dvdn_gt0 m_dv_a.
+have oam: #|<[a ^+ (#[a] %/ m)]>| = m.
+  apply/eqP; rewrite [#|_|]orderXgcd -(divnMr m_gt0) muln_gcdl divnK //.
+  by rewrite gcdnC gcdnMr mulKn.
+apply/eqP; rewrite eqEsubset sub1set inE /= cycleX oam eqxx !andbT.
+apply/subsetP=> X; rewrite in_set1 inE -val_eqE /= eqEcard oam.
+case/andP=> sXa /eqP oX; rewrite oX leqnn andbT.
+apply/subsetP=> x Xx; case/cycleP: (subsetP sXa _ Xx) => k def_x.
+have: (x ^+ m == 1)%g by rewrite -oX -order_dvdn cardSg // gen_subG sub1set.
+rewrite {x Xx}def_x -expgM -order_dvdn -[#[a]](Lagrange sXa) -oX mulnC.
+rewrite dvdn_pmul2r // mulnK // => /dvdnP[i ->].
+by rewrite mulnC expgM groupX // cycle_id.
+Qed.
+
+Lemma cycle_subgroup_char a (H : {group gT}) : H \subset <[a]> -> H \char <[a]>.
+Proof.
+move=> sHa; apply: lone_subgroup_char => // J sJa isoJH.
+have dvHa: #|H| %| #[a] by exact: cardSg.
+have{dvHa} /setP Huniq := esym (cycle_sub_group dvHa).
+move: (Huniq H) (Huniq J); rewrite !inE /=.
+by rewrite sHa sJa (card_isog isoJH) eqxx => /eqP<- /eqP<-.
+Qed.
+
+End CycleSubGroup.
+
+(***********************************************************************)
+(*  Reflected boolean property and morphic image, injection, bijection *)
+(***********************************************************************)
+
+Section MorphicImage.
+
+Variables aT rT : finGroupType.
+Variables (D : {group aT}) (f : {morphism D >-> rT}) (x : aT).
+Hypothesis Dx : x \in D.
+
+Lemma morph_order : #[f x] %| #[x].
+Proof. by rewrite order_dvdn -morphX // expg_order morph1. Qed.
+
+Lemma morph_generator A : generator A x -> generator (f @* A) (f x).
+Proof. by move/(A =P _)->; rewrite /generator morphim_cycle. Qed.
+
+End MorphicImage.
+
+Section CyclicProps.
+
+Variables gT : finGroupType.
+Implicit Types (aT rT : finGroupType) (G H K : {group gT}).
+
+Lemma cyclicS G H : H \subset G -> cyclic G -> cyclic H.
+Proof.
+move=> sHG /cyclicP[x defG]; apply/cyclicP.
+exists (x ^+ (#[x] %/ #|H|)); apply/congr_group/set1P.
+by rewrite -cycle_sub_group /order -defG ?cardSg // inE sHG eqxx.
+Qed.
+
+Lemma cyclicJ G x : cyclic (G :^ x) = cyclic G.
+Proof.
+apply/cyclicP/cyclicP=> [[y /(canRL (conjsgK x))] | [y ->]].
+  by rewrite -cycleJ; exists (y ^ x^-1).
+by exists (y ^ x); rewrite cycleJ.
+Qed.
+
+Lemma eq_subG_cyclic G H K :
+  cyclic G -> H \subset G -> K \subset G -> (H :==: K) = (#|H| == #|K|).
+Proof.
+case/cyclicP=> x -> sHx sKx; apply/eqP/eqP=> [-> //| eqHK].
+have def_GHx := cycle_sub_group (cardSg sHx); set GHx := [set _] in def_GHx.
+have []: H \in GHx /\ K \in GHx by rewrite -def_GHx !inE sHx sKx eqHK /=.
+by do 2!move/set1P->.
+Qed.
+
+Lemma cardSg_cyclic G H K :
+  cyclic G -> H \subset G -> K \subset G -> (#|H| %| #|K|) = (H \subset K).
+Proof.
+move=> cycG sHG sKG; apply/idP/idP; last exact: cardSg.
+case/cyclicP: (cyclicS sKG cycG) => x defK; rewrite {K}defK in sKG *.
+case/dvdnP=> k ox; suffices ->: H :=: <[x ^+ k]> by exact: cycleX.
+apply/eqP; rewrite (eq_subG_cyclic cycG) ?(subset_trans (cycleX _ _)) //.
+rewrite -orderE orderXdiv orderE ox ?dvdn_mulr ?mulKn //.
+by have:= order_gt0 x; rewrite orderE ox; case k.
+Qed.
+
+Lemma sub_cyclic_char G H : cyclic G -> (H \char G) = (H \subset G).
+Proof.
+case/cyclicP=> x ->; apply/idP/idP => [/andP[] //|].
+exact: cycle_subgroup_char.
+Qed.
+
+Lemma morphim_cyclic rT G H (f : {morphism G >-> rT}) :
+  cyclic H -> cyclic (f @* H).
+Proof.
+move=> cycH; wlog sHG: H cycH / H \subset G.
+  by rewrite -morphimIdom; apply; rewrite (cyclicS _ cycH, subsetIl) ?subsetIr.
+case/cyclicP: cycH sHG => x ->; rewrite gen_subG sub1set => Gx.
+by apply/cyclicP; exists (f x); rewrite morphim_cycle.
+Qed.
+
+Lemma quotient_cycle x H : x \in 'N(H) -> <[x]> / H = <[coset H x]>.
+Proof. exact: morphim_cycle. Qed.
+
+Lemma quotient_cyclic G H : cyclic G -> cyclic (G / H).
+Proof. exact: morphim_cyclic. Qed.
+
+Lemma quotient_generator x G H :
+  x \in 'N(H) -> generator G x -> generator (G / H) (coset H x).
+Proof. by move=> Nx; apply: morph_generator. Qed.
+
+Lemma prime_cyclic G : prime #|G| -> cyclic G.
+Proof.
+case/primeP; rewrite ltnNge -trivg_card_le1.
+case/trivgPn=> x Gx ntx /(_ _ (order_dvdG Gx)).
+rewrite order_eq1 (negbTE ntx) => /eqnP oxG; apply/cyclicP.
+by exists x; apply/eqP; rewrite eq_sym eqEcard -oxG cycle_subG Gx leqnn.
+Qed.
+
+Lemma dvdn_prime_cyclic G p : prime p -> #|G| %| p -> cyclic G.
+Proof.
+move=> p_pr pG; case: (eqsVneq G 1) => [-> | ntG]; first exact: cyclic1.
+by rewrite prime_cyclic // (prime_nt_dvdP p_pr _ pG) -?trivg_card1.
+Qed.
+
+Lemma cyclic_small G : #|G| <= 3 -> cyclic G.
+Proof.
+rewrite 4!(ltnS, leq_eqVlt) -trivg_card_le1 orbA orbC.
+case/predU1P=> [-> | oG]; first exact: cyclic1.
+by apply: prime_cyclic; case/pred2P: oG => ->.
+Qed.
+
+End CyclicProps.
+
+Section IsoCyclic.
+
+Variables gT rT : finGroupType.
+Implicit Types (G H : {group gT}) (M : {group rT}).
+
+Lemma injm_cyclic G H (f : {morphism G >-> rT}) :
+  'injm f -> H \subset G -> cyclic (f @* H) = cyclic H.
+Proof.
+move=> injf sHG; apply/idP/idP; last exact: morphim_cyclic.
+rewrite -{2}(morphim_invm injf sHG); exact: morphim_cyclic.
+Qed.
+
+Lemma isog_cyclic G M : G \isog M -> cyclic G = cyclic M.
+Proof. by case/isogP=> f injf <-; rewrite injm_cyclic. Qed.
+
+Lemma isog_cyclic_card G M : cyclic G -> isog G M = cyclic M && (#|M| == #|G|).
+Proof.
+move=> cycG; apply/idP/idP=> [isoGM | ].
+  by rewrite (card_isog isoGM) -(isog_cyclic isoGM) cycG /=.
+case/cyclicP: cycG => x ->{G} /andP[/cyclicP[y ->] /eqP oy].
+by apply: isog_trans (isog_symr _) (Zp_isog y); rewrite /order oy Zp_isog.
+Qed.
+
+Lemma injm_generator G H (f : {morphism G >-> rT}) x :
+    'injm f -> x \in G -> H \subset G ->
+  generator (f @* H) (f x) = generator H x.
+Proof.
+move=> injf Gx sHG; apply/idP/idP; last exact: morph_generator.
+rewrite -{2}(morphim_invm injf sHG) -{2}(invmE injf Gx).
+by apply: morph_generator; exact: mem_morphim.
+Qed.
+
+End IsoCyclic.
+
+(* Metacyclic groups. *)
+Section Metacyclic.
+
+Variable gT : finGroupType.
+Implicit Types (A : {set gT}) (G H : {group gT}).
+
+Definition metacyclic A :=
+  [exists H : {group gT}, [&& cyclic H, H <| A & cyclic (A / H)]].
+
+Lemma metacyclicP A : 
+  reflect (exists H : {group gT}, [/\ cyclic H, H <| A & cyclic (A / H)]) 
+          (metacyclic A).
+Proof. exact: 'exists_and3P. Qed.
+
+Lemma metacyclic1 : metacyclic 1.
+Proof. 
+by apply/existsP; exists 1%G; rewrite normal1 trivg_quotient !cyclic1.
+Qed.
+
+Lemma cyclic_metacyclic A : cyclic A -> metacyclic A.
+Proof.
+case/cyclicP=> x ->; apply/existsP; exists (<[x]>)%G.
+by rewrite normal_refl cycle_cyclic trivg_quotient cyclic1.
+Qed.
+
+Lemma metacyclicS G H : H \subset G -> metacyclic G -> metacyclic H.
+Proof.
+move=> sHG /metacyclicP[K [cycK nsKG cycGq]]; apply/metacyclicP.
+exists (H :&: K)%G; rewrite (cyclicS (subsetIr H K)) ?(normalGI sHG) //=.
+rewrite setIC (isog_cyclic (second_isog _)) ?(cyclicS _ cycGq) ?quotientS //.
+by rewrite (subset_trans sHG) ?normal_norm.
+Qed.
+
+End Metacyclic.
+
+Arguments Scope metacyclic [_ group_scope].
+Prenex Implicits metacyclic.
+Implicit Arguments metacyclicP [gT A].
+
+(* Automorphisms of cyclic groups. *)
+Section CyclicAutomorphism.
+
+Variable gT : finGroupType.
+
+Section CycleAutomorphism.
+
+Variable a : gT.
+
+Section CycleMorphism.
+
+Variable n : nat.
+
+Definition cyclem of gT := fun x : gT => x ^+ n.
+
+Lemma cyclemM : {in <[a]> & , {morph cyclem a : x y / x * y}}.
+Proof.
+by move=> x y ax ay; apply: expgMn; exact: (centsP (cycle_abelian a)).
+Qed.
+
+Canonical cyclem_morphism := Morphism cyclemM.
+
+End CycleMorphism.
+
+Section ZpUnitMorphism.
+
+Variable u : {unit 'Z_#[a]}.
+
+Lemma injm_cyclem : 'injm (cyclem (val u) a).
+Proof.
+apply/subsetP=> x /setIdP[ax]; rewrite !inE -order_dvdn.
+case: (eqVneq a 1) => [a1 | nta]; first by rewrite a1 cycle1 inE in ax.
+rewrite -order_eq1 -dvdn1; move/eqnP: (valP u) => /= <-.
+by rewrite dvdn_gcd {2}Zp_cast ?order_gt1 // order_dvdG.
+Qed.
+
+Lemma im_cyclem : cyclem (val u) a @* <[a]> = <[a]>.
+Proof.
+apply/morphim_fixP=> //; first exact: injm_cyclem.
+by rewrite morphim_cycle ?cycle_id ?cycleX.
+Qed.
+
+Definition Zp_unitm := aut injm_cyclem im_cyclem.
+
+End ZpUnitMorphism.
+
+Lemma Zp_unitmM : {in units_Zp #[a] &, {morph Zp_unitm : u v / u * v}}.
+Proof.
+move=> u v _ _; apply: (eq_Aut (Aut_aut _ _)) => [|x a_x].
+  by rewrite groupM ?Aut_aut.
+rewrite permM !autE ?groupX //= /cyclem -expgM.
+rewrite -expg_mod_order modn_dvdm ?expg_mod_order //.
+case: (leqP #[a] 1) => [lea1 | lt1a]; last by rewrite Zp_cast ?order_dvdG.
+by rewrite card_le1_trivg // in a_x; rewrite (set1P a_x) order1 dvd1n.
+Qed.
+
+Canonical Zp_unit_morphism := Morphism Zp_unitmM.
+
+Lemma injm_Zp_unitm : 'injm Zp_unitm.
+Proof.
+case: (eqVneq a 1) => [a1 | nta].
+  by rewrite subIset //= card_le1_trivg ?subxx // card_units_Zp a1 order1.
+apply/subsetP=> /= u /morphpreP[_ /set1P/= um1].
+have{um1}: Zp_unitm u a == Zp_unitm 1 a by rewrite um1 morph1.
+rewrite !autE ?cycle_id // eq_expg_mod_order.
+by rewrite -[n in _ == _ %[mod n]]Zp_cast ?order_gt1 // !modZp inE.
+Qed.
+
+Lemma generator_coprime m : generator <[a]> (a ^+ m) = coprime #[a] m.
+Proof.
+rewrite /generator eq_sym eqEcard cycleX -/#[a] [#|_|]orderXgcd /=.
+apply/idP/idP=> [le_a_am|co_am]; last by rewrite (eqnP co_am) divn1.
+have am_gt0: 0 < gcdn #[a] m by rewrite gcdn_gt0 order_gt0.
+by rewrite /coprime eqn_leq am_gt0 andbT -(@leq_pmul2l #[a]) ?muln1 -?leq_divRL.
+Qed.
+
+Lemma im_Zp_unitm : Zp_unitm @* units_Zp #[a] = Aut <[a]>.
+Proof.
+rewrite morphimEdom; apply/setP=> f; pose n := invm (injm_Zpm a) (f a).
+apply/imsetP/idP=> [[u _ ->] | Af]; first exact: Aut_aut.
+have [a1 | nta] := eqVneq a 1.
+  by rewrite a1 cycle1 Aut1 in Af; exists 1; rewrite // morph1 (set1P Af).
+have a_fa: <[a]> = <[f a]>.
+  by rewrite -(autmE Af) -morphim_cycle ?im_autm ?cycle_id.
+have def_n: a ^+ n = f a.
+  by rewrite -/(Zpm n) invmK // im_Zpm a_fa cycle_id.
+have co_a_n: coprime #[a].-2.+2 n.
+  by rewrite {1}Zp_cast ?order_gt1 // -generator_coprime def_n; exact/eqP.
+exists (FinRing.unit 'Z_#[a] co_a_n); rewrite ?inE //.
+apply: eq_Aut (Af) (Aut_aut _ _) _ => x ax.
+rewrite autE //= /cyclem; case/cycleP: ax => k ->{x}.
+by rewrite -(autmE Af) morphX ?cycle_id //= autmE -def_n -!expgM mulnC.
+Qed.
+
+Lemma Zp_unit_isom : isom (units_Zp #[a]) (Aut <[a]>) Zp_unitm.
+Proof. by apply/isomP; rewrite ?injm_Zp_unitm ?im_Zp_unitm. Qed.
+
+Lemma Zp_unit_isog : isog (units_Zp #[a]) (Aut <[a]>).
+Proof. exact: isom_isog Zp_unit_isom. Qed.
+
+Lemma card_Aut_cycle : #|Aut <[a]>| = totient #[a].
+Proof. by rewrite -(card_isog Zp_unit_isog) card_units_Zp. Qed.
+
+Lemma totient_gen : totient #[a] = #|[set x | generator <[a]> x]|.
+Proof.
+have [lea1 | lt1a] := leqP #[a] 1.
+  rewrite /order card_le1_trivg // cards1 (@eq_card1 _ 1) // => x.
+  by rewrite !inE -cycle_eq1 eq_sym.
+rewrite -(card_injm (injm_invm (injm_Zpm a))) /= ?im_Zpm; last first.
+  by apply/subsetP=> x; rewrite inE; exact: cycle_generator.
+rewrite -card_units_Zp // cardsE card_sub morphim_invmE; apply: eq_card => /= d.
+by rewrite !inE /= qualifE /= /Zp lt1a inE /= generator_coprime {1}Zp_cast.
+Qed.
+
+Lemma Aut_cycle_abelian : abelian (Aut <[a]>).
+Proof. by rewrite -im_Zp_unitm morphim_abelian ?units_Zp_abelian. Qed.
+
+End CycleAutomorphism.
+
+Variable G : {group gT}.
+
+Lemma Aut_cyclic_abelian : cyclic G -> abelian (Aut G).
+Proof. by case/cyclicP=> x ->; exact: Aut_cycle_abelian. Qed.
+
+Lemma card_Aut_cyclic : cyclic G -> #|Aut G| = totient #|G|.
+Proof. by case/cyclicP=> x ->; exact: card_Aut_cycle. Qed.
+
+Lemma sum_ncycle_totient :
+  \sum_(d < #|G|.+1) #|[set <[x]> | x in G & #[x] == d]| * totient d = #|G|.
+Proof.
+pose h (x : gT) : 'I_#|G|.+1 := inord #[x].
+symmetry; rewrite -{1}sum1_card (partition_big h xpredT) //=.
+apply: eq_bigr => d _; set Gd := finset _.
+rewrite -sum_nat_const sum1dep_card -sum1_card (_ : finset _ = Gd); last first.
+  apply/setP=> x; rewrite !inE; apply: andb_id2l => Gx.
+  by rewrite /eq_op /= inordK // ltnS subset_leq_card ?cycle_subG.
+rewrite (partition_big_imset cycle) {}/Gd; apply: eq_bigr => C /=.
+case/imsetP=> x /setIdP[Gx /eqP <-] -> {C d}.
+rewrite sum1dep_card totient_gen; apply: eq_card => y; rewrite !inE /generator.
+move: Gx; rewrite andbC eq_sym -!cycle_subG /order.
+by case: eqP => // -> ->; rewrite eqxx.
+Qed.
+
+End CyclicAutomorphism.
+
+Lemma sum_totient_dvd n : \sum_(d < n.+1 | d %| n) totient d = n.
+Proof.
+case: n => [|[|n']]; try by rewrite big_mkcond !big_ord_recl big_ord0.
+set n := n'.+2; pose x1 : 'Z_n := 1%R.
+have ox1: #[x1] = n by rewrite /order -Zp_cycle card_Zp.
+rewrite -[rhs in _ = rhs]ox1 -[#[_]]sum_ncycle_totient [#|_|]ox1 big_mkcond /=.
+apply: eq_bigr => d _; rewrite -{2}ox1; case: ifP => [|ndv_dG]; last first.
+  rewrite eq_card0 // => C; apply/imsetP=> [[x /setIdP[Gx oxd] _{C}]].
+  by rewrite -(eqP oxd) order_dvdG in ndv_dG.
+move/cycle_sub_group; set Gd := [set _] => def_Gd.
+rewrite (_ : _ @: _ = @gval _ @: Gd); first by rewrite imset_set1 cards1 mul1n.
+apply/setP=> C; apply/idP/imsetP=> [| [gC GdC ->{C}]].
+  case/imsetP=> x /setIdP[_ oxd] ->; exists <[x]>%G => //.
+  by rewrite -def_Gd inE -Zp_cycle subsetT.
+have:= GdC; rewrite -def_Gd => /setIdP[_ /eqP <-].
+by rewrite (set1P GdC) /= mem_imset // inE eqxx (mem_cycle x1).
+Qed.
+
+Section FieldMulCyclic.
+
+(***********************************************************************)
+(* A classic application to finite multiplicative subgroups of fields. *)
+(***********************************************************************)
+
+Import GRing.Theory.
+
+Variables (gT : finGroupType) (G : {group gT}).
+
+Lemma order_inj_cyclic :
+  {in G &, forall x y, #[x] = #[y] -> <[x]> = <[y]>} -> cyclic G.
+Proof.
+move=> ucG; apply: negbNE (contra _ (negbT (ltnn #|G|))) => ncG.
+rewrite -{2}[#|G|]sum_totient_dvd big_mkcond (bigD1 ord_max) ?dvdnn //=.
+rewrite -{1}[#|G|]sum_ncycle_totient (bigD1 ord_max) //= -addSn leq_add //.
+  rewrite eq_card0 ?totient_gt0 ?cardG_gt0 // => C.
+  apply/imsetP=> [[x /setIdP[Gx /eqP oxG]]]; case/cyclicP: ncG.
+  by exists x; apply/eqP; rewrite eq_sym eqEcard cycle_subG Gx -oxG /=.
+elim/big_ind2: _ => // [m1 n1 m2 n2 | d _]; first exact: leq_add.
+set Gd := _ @: _; case: (set_0Vmem Gd) => [-> | [C]]; first by rewrite cards0.
+rewrite {}/Gd => /imsetP[x /setIdP[Gx /eqP <-] _ {C d}].
+rewrite order_dvdG // (@eq_card1 _ <[x]>) ?mul1n // => C.
+apply/idP/eqP=> [|-> {C}]; last by rewrite mem_imset // inE Gx eqxx.
+by case/imsetP=> y /setIdP[Gy /eqP/ucG->].
+Qed.
+
+Lemma div_ring_mul_group_cyclic (R : unitRingType) (f : gT -> R) :
+    f 1 = 1%R -> {in G &, {morph f : u v / u * v >-> (u * v)%R}} ->
+    {in G^#, forall x, f x - 1 \in GRing.unit}%R ->
+  abelian G -> cyclic G.
+Proof.
+move=> f1 fM f1P abelG.
+have fX n: {in G, {morph f : u / u ^+ n >-> (u ^+ n)%R}}.
+  by case: n => // n x Gx; elim: n => //= n IHn; rewrite expgS fM ?groupX ?IHn.
+have fU x: x \in G -> f x \in GRing.unit.
+  by move=> Gx; apply/unitrP; exists (f x^-1); rewrite -!fM ?groupV ?gsimp.
+apply: order_inj_cyclic => x y Gx Gy; set n := #[x] => yn.
+apply/eqP; rewrite eq_sym eqEcard -[#|_|]/n yn leqnn andbT cycle_subG /=.
+suff{y Gy yn} ->: <[x]> = G :&: [set z | #[z] %| n] by rewrite !inE Gy yn /=.
+apply/eqP; rewrite eqEcard subsetI cycle_subG {}Gx /= cardE; set rs := enum _.
+apply/andP; split; first by apply/subsetP=> y xy; rewrite inE order_dvdG.
+pose P : {poly R} := ('X^n - 1)%R; have n_gt0: n > 0 by exact: order_gt0.
+have szP: size P = n.+1 by rewrite size_addl size_polyXn ?size_opp ?size_poly1.
+rewrite -ltnS -szP -(size_map f) max_ring_poly_roots -?size_poly_eq0 ?{}szP //.
+  apply/allP=> fy /mapP[y]; rewrite mem_enum !inE order_dvdn => /andP[Gy].
+  move/eqP=> yn1 ->{fy}; apply/eqP.
+  by rewrite !(hornerE, hornerXn) -fX // yn1 f1 subrr.
+have: uniq rs by exact: enum_uniq.
+have: all (mem G) rs by apply/allP=> y; rewrite mem_enum; case/setIP.
+elim: rs => //= y rs IHrs /andP[Gy Grs] /andP[y_rs]; rewrite andbC.
+move/IHrs=> -> {IHrs}//; apply/allP=> _ /mapP[z rs_z ->].
+have{Grs} Gz := allP Grs z rs_z; rewrite /diff_roots -!fM // (centsP abelG) //.
+rewrite eqxx -[f y]mul1r -(mulgKV y z) fM ?groupM ?groupV //=.
+rewrite -mulNr -mulrDl unitrMl ?fU ?f1P // !inE.
+by rewrite groupM ?groupV // andbT -eq_mulgV1; apply: contra y_rs; move/eqP <-.
+Qed.
+
+Lemma field_mul_group_cyclic (F : fieldType) (f : gT -> F) :
+    {in G &, {morph f : u v / u * v >-> (u * v)%R}} ->
+    {in G, forall x, f x = 1%R <-> x = 1} ->
+  cyclic G.
+Proof.
+move=> fM f1P; have f1 : f 1 = 1%R by exact/f1P.
+apply: (div_ring_mul_group_cyclic f1 fM) => [x|].
+  case/setD1P=> x1 Gx; rewrite unitfE; apply: contra x1.
+  by rewrite subr_eq0 => /eqP/f1P->.
+apply/centsP=> x Gx y Gy; apply/commgP/eqP.
+apply/f1P; rewrite ?fM ?groupM ?groupV //.
+by rewrite mulrCA -!fM ?groupM ?groupV // mulKg mulVg.
+Qed.
+
+End FieldMulCyclic.
+
+Lemma field_unit_group_cyclic (F : finFieldType) (G : {group {unit F}}) :
+  cyclic G.
+Proof.
+apply: field_mul_group_cyclic FinRing.uval _ _ => // u _.
+by split=> /eqP ?; exact/eqP.
+Qed.
+
+Section PrimitiveRoots.
+
+Open Scope ring_scope.
+Import GRing.Theory.
+
+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.
+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.
+pose sgT := BaseFinGroupType _ (FinGroup.Mixin sG_Ag sG_1g sG_Vg).
+pose gT := @FinGroupType sgT sG_Vg.
+have /cyclicP[x gen_x]: @cyclic gT setT.
+  apply: (@field_mul_group_cyclic gT [set: _] F r) => // x _.
+  by split=> [ri1 | ->]; first exact: val_inj.
+apply/hasP; exists (r x); first exact: (valP x).
+have [m prim_x dvdmn] := prim_order_exists n_gt0 (rn1 x).
+rewrite -((m =P n) _) // eqn_dvd {}dvdmn -sz_rs -(card_seq_sub Urs) -cardsT.
+rewrite gen_x (@order_dvdn gT) /(_ == _) /= -{prim_x}(prim_expr_order prim_x).
+by apply/eqP; elim: m => //= m IHm; rewrite exprS expgS /= -IHm.
+Qed.
+
+End PrimitiveRoots.
+
+(***********************************************************************)
+(*  Cycles of prime order                                              *)
+(***********************************************************************)
+
+Section AutPrime.
+
+Variable gT : finGroupType.
+
+Lemma Aut_prime_cycle_cyclic (a : gT) : prime #[a] -> cyclic (Aut <[a]>).
+Proof.
+move=> pr_a; have inj_um := injm_Zp_unitm a; have 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.
+
+Lemma Aut_prime_cyclic (G : {group gT}) : prime #|G| -> cyclic (Aut G).
+Proof.
+move=> pr_G; case/cyclicP: (prime_cyclic pr_G) (pr_G) => x ->.
+exact: Aut_prime_cycle_cyclic.
+Qed.
+
+End AutPrime.
diff --git a/mathcomp/algebra/opam b/mathcomp/algebra/opam
new file mode 100644
index 0000000..f662b48
--- /dev/null
+++ b/mathcomp/algebra/opam
@@ -0,0 +1,12 @@
+opam-version: "1.2"
+name: "coq:mathcomp:algebra"
+version: "1.5"
+maintainer: "Ssreflect <ssreflect@msr-inria.inria.fr>"
+authors: "Ssreflect <ssreflect@msr-inria.inria.fr>"
+homepage: "http://ssr.msr-inria.inria.fr/"
+bug-reports: "ssreflect@msr-inria.inria.fr"
+license: "CeCILL-B"
+build: [ make "-j" "%{jobs}%" ] 
+install: [ make "install" ]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/algebra'" ]
+depends: [ "coq:mathcomp:fingroup" { = "1.5" } ]
diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v
new file mode 100644
index 0000000..df5b378
--- /dev/null
+++ b/mathcomp/algebra/zmodp.v
@@ -0,0 +1,362 @@
+(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
+Require Import fintype bigop finset prime fingroup ssralg finalg.
+
+(******************************************************************************)
+(*  Definition of the additive group and ring Zp, represented as 'I_p         *)
+(******************************************************************************)
+(* Definitions:                                                               *)
+(* From fintype.v:                                                            *)
+(*     'I_p == the subtype of integers less than p, taken here as the type of *)
+(*             the integers mod p.                                            *)
+(* This file:                                                                 *)
+(*     inZp == the natural projection from nat into the integers mod p,       *)
+(*             represented as 'I_p. Here p is implicit, but MUST be of the    *)
+(*             form n.+1.                                                     *)
+(* The operations:                                                            *)
+(*      Zp0 == the identity element for addition                              *)
+(*      Zp1 == the identity element for multiplication, and a generator of    *)
+(*             additive group                                                 *)
+(*   Zp_opp == inverse function for addition                                  *)
+(*   Zp_add == addition                                                       *)
+(*   Zp_mul == multiplication                                                 *)
+(*   Zp_inv == inverse function for multiplication                            *)
+(* Note that while 'I_n.+1 has canonical finZmodType and finGroupType         *)
+(* structures, only 'I_n.+2 has a canonical ring structure (it has, in fact,  *)
+(* a canonical finComUnitRing structure), and hence an associated             *)
+(* multiplicative unit finGroupType. To mitigate the issues caused by the     *)
+(* trivial "ring" (which is, indeed is NOT a ring in the ssralg/finalg        *)
+(* formalization), we define additional notation:                             *)
+(*       'Z_p == the type of integers mod (max p 2); this is always a proper  *)
+(*               ring, by constructions. Note that 'Z_p is provably equal to  *)
+(*               'I_p if p > 1, and convertible to 'I_p if p is of the form   *)
+(*               n.+2.                                                        *)
+(*       Zp p == the subgroup of integers mod (max p 1) in 'Z_p; this is thus *)
+(*               is thus all of 'Z_p if p > 1, and else the trivial group.    *)
+(* units_Zp p == the group of all units of 'Z_p -- i.e., the group of         *)
+(*               (multiplicative) automorphisms of Zp p.                      *)
+(* We show that Zp and units_Zp are abelian, and compute their orders.        *)
+(* We use a similar technique to represent the prime fields:                  *)
+(*        'F_p == the finite field of integers mod the first prime divisor of *)
+(*                maxn p 2. This is provably equal to 'Z_p and 'I_p if p is   *)
+(*                provably prime, and indeed convertible to the above if p is *)
+(*                a concrete prime such as 2, 5 or 23.                        *)
+(* Note finally that due to the canonical structures it is possible to use    *)
+(* 0%R instead of Zp0, and 1%R instead of Zp1 (for the latter, p must be of   *)
+(* the form n.+2, and 1%R : nat will simplify to 1%N).                        *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope ring_scope.
+
+Section ZpDef.
+
+(***********************************************************************)
+(*                                                                     *)
+(*  Mod p arithmetic on the finite set {0, 1, 2, ..., p - 1}           *)
+(*                                                                     *)
+(***********************************************************************)
+
+Variable p' : nat.
+Local Notation p := p'.+1.
+
+Implicit Types x y z : 'I_p.
+
+(* Standard injection; val (inZp i) = i %% p *)
+Definition inZp i := Ordinal (ltn_pmod i (ltn0Sn p')).
+Lemma modZp x : x %% p = x.
+Proof. by rewrite modn_small ?ltn_ord. Qed.
+Lemma valZpK x : inZp x = x.
+Proof. by apply: val_inj; rewrite /= modZp. Qed.
+
+(* Operations *)
+Definition Zp0 : 'I_p := ord0.
+Definition Zp1 := inZp 1.
+Definition Zp_opp x := inZp (p - x).
+Definition Zp_add x y := inZp (x + y).
+Definition Zp_mul x y := inZp (x * y).
+Definition Zp_inv x := if coprime p x then inZp (egcdn x p).1 else x.
+
+(* Additive group structure. *)
+
+Lemma Zp_add0z : left_id Zp0 Zp_add.
+Proof. exact: valZpK. Qed.
+
+Lemma Zp_addNz : left_inverse Zp0 Zp_opp Zp_add.
+Proof.
+by move=> x; apply: val_inj; rewrite /= modnDml subnK ?modnn // ltnW.
+Qed.
+
+Lemma Zp_addA : associative Zp_add.
+Proof.
+by move=> x y z; apply: val_inj; rewrite /= modnDml modnDmr addnA.
+Qed.
+
+Lemma Zp_addC : commutative Zp_add.
+Proof. by move=> x y; apply: val_inj; rewrite /= addnC. Qed.
+
+Definition Zp_zmodMixin := ZmodMixin Zp_addA Zp_addC Zp_add0z Zp_addNz.
+Canonical Zp_zmodType := Eval hnf in ZmodType 'I_p Zp_zmodMixin.
+Canonical Zp_finZmodType := Eval hnf in [finZmodType of 'I_p].
+Canonical Zp_baseFinGroupType := Eval hnf in [baseFinGroupType of 'I_p for +%R].
+Canonical Zp_finGroupType := Eval hnf in [finGroupType of 'I_p for +%R].
+
+(* Ring operations *)
+
+Lemma Zp_mul1z : left_id Zp1 Zp_mul.
+Proof. by move=> x; apply: val_inj; rewrite /= modnMml mul1n modZp. Qed.
+
+Lemma Zp_mulC : commutative Zp_mul.
+Proof. by move=> x y; apply: val_inj; rewrite /= mulnC. Qed.
+
+Lemma Zp_mulz1 : right_id Zp1 Zp_mul.
+Proof. by move=> x; rewrite Zp_mulC Zp_mul1z. Qed.
+
+Lemma Zp_mulA : associative Zp_mul.
+Proof.
+by move=> x y z; apply: val_inj; rewrite /= modnMml modnMmr mulnA.
+Qed.
+
+Lemma Zp_mul_addr : right_distributive Zp_mul Zp_add.
+Proof.
+by move=> x y z; apply: val_inj; rewrite /= modnMmr modnDm mulnDr.
+Qed.
+
+Lemma Zp_mul_addl : left_distributive Zp_mul Zp_add.
+Proof. by move=> x y z; rewrite -!(Zp_mulC z) Zp_mul_addr. Qed.
+
+Lemma Zp_mulVz x : coprime p x -> Zp_mul (Zp_inv x) x = Zp1.
+Proof.
+move=> co_p_x; apply: val_inj; rewrite /Zp_inv co_p_x /= modnMml.
+by rewrite -(chinese_modl co_p_x 1 0) /chinese addn0 mul1n mulnC.
+Qed.
+
+Lemma Zp_mulzV x : coprime p x -> Zp_mul x (Zp_inv x) = Zp1.
+Proof. by move=> Ux; rewrite /= Zp_mulC Zp_mulVz. Qed.
+
+Lemma Zp_intro_unit x y : Zp_mul y x = Zp1 -> coprime p x.
+Proof.
+case=> yx1; have:= coprimen1 p.
+by rewrite -coprime_modr -yx1 coprime_modr coprime_mulr; case/andP.
+Qed.
+
+Lemma Zp_inv_out x : ~~ coprime p x -> Zp_inv x = x.
+Proof. by rewrite /Zp_inv => /negPf->. Qed.
+
+Lemma Zp_mulrn x n : x *+ n = inZp (x * n).
+Proof.
+apply: val_inj => /=; elim: n => [|n IHn]; first by rewrite muln0 modn_small.
+by rewrite !GRing.mulrS /= IHn modnDmr mulnS.
+Qed.
+
+Import GroupScope.
+
+Lemma Zp_mulgC : @commutative 'I_p _ mulg.
+Proof. exact: Zp_addC. Qed.
+
+Lemma Zp_abelian : abelian [set: 'I_p].
+Proof. exact: FinRing.zmod_abelian. Qed.
+
+Lemma Zp_expg x n : x ^+ n = inZp (x * n).
+Proof. exact: Zp_mulrn. Qed.
+
+Lemma Zp1_expgz x : Zp1 ^+ x = x.
+Proof. by rewrite Zp_expg; exact: Zp_mul1z. Qed.
+
+Lemma Zp_cycle : setT = <[Zp1]>.
+Proof. by apply/setP=> x; rewrite -[x]Zp1_expgz inE groupX ?mem_gen ?set11. Qed.
+
+Lemma order_Zp1 : #[Zp1] = p.
+Proof. by rewrite orderE -Zp_cycle cardsT card_ord. Qed.
+
+End ZpDef.
+
+Implicit Arguments Zp0 [[p']].
+Implicit Arguments Zp1 [[p']].
+Implicit Arguments inZp [[p']].
+
+Lemma ord1 : all_equal_to (0 : 'I_1).
+Proof. by case=> [[] // ?]; exact: val_inj. Qed.
+
+Lemma lshift0 m n : lshift m (0 : 'I_n.+1) = (0 : 'I_(n + m).+1).
+Proof. exact: val_inj. Qed.
+
+Lemma rshift1 n : @rshift 1 n =1 lift (0 : 'I_n.+1).
+Proof. by move=> i; exact: val_inj. Qed.
+
+Lemma split1 n i :
+  split (i : 'I_(1 + n)) = oapp (@inr _ _) (inl _ 0) (unlift 0 i).
+Proof.
+case: unliftP => [i'|] -> /=.
+  by rewrite -rshift1 (unsplitK (inr _ _)).
+by rewrite -(lshift0 n 0) (unsplitK (inl _ _)).
+Qed.
+
+Lemma big_ord1 R idx (op : @Monoid.law R idx) F :
+  \big[op/idx]_(i < 1) F i = F 0.
+Proof. by rewrite big_ord_recl big_ord0 Monoid.mulm1. Qed.
+
+Lemma big_ord1_cond R idx (op : @Monoid.law R idx) P F :
+  \big[op/idx]_(i < 1 | P i) F i = if P 0 then F 0 else idx.
+Proof. by rewrite big_mkcond big_ord1. Qed.
+
+Section ZpRing.
+
+Variable p' : nat.
+Local Notation p := p'.+2.
+
+Lemma Zp_nontrivial : Zp1 != 0 :> 'I_p. Proof. by []. Qed.
+
+Definition Zp_ringMixin :=
+  ComRingMixin (@Zp_mulA _) (@Zp_mulC _) (@Zp_mul1z _) (@Zp_mul_addl _)
+               Zp_nontrivial.
+Canonical Zp_ringType := Eval hnf in RingType 'I_p Zp_ringMixin.
+Canonical Zp_finRingType := Eval hnf in [finRingType of 'I_p].
+Canonical Zp_comRingType := Eval hnf in ComRingType 'I_p (@Zp_mulC _).
+Canonical Zp_finComRingType := Eval hnf in [finComRingType of 'I_p].
+
+Definition Zp_unitRingMixin :=
+  ComUnitRingMixin (@Zp_mulVz _) (@Zp_intro_unit _) (@Zp_inv_out _).
+Canonical Zp_unitRingType := Eval hnf in UnitRingType 'I_p Zp_unitRingMixin.
+Canonical Zp_finUnitRingType := Eval hnf in [finUnitRingType of 'I_p].
+Canonical Zp_comUnitRingType := Eval hnf in [comUnitRingType of 'I_p].
+Canonical Zp_finComUnitRingType := Eval hnf in [finComUnitRingType of 'I_p].
+
+Lemma Zp_nat n : n%:R = inZp n :> 'I_p.
+Proof. by apply: val_inj; rewrite [n%:R]Zp_mulrn /= modnMml mul1n. Qed.
+
+Lemma natr_Zp (x : 'I_p) : x%:R = x.
+Proof. by rewrite Zp_nat valZpK. Qed.
+
+Lemma natr_negZp (x : 'I_p) : (- x)%:R = - x.
+Proof. by apply: val_inj; rewrite /= Zp_nat /= modn_mod. Qed.
+
+Import GroupScope.
+
+Lemma unit_Zp_mulgC : @commutative {unit 'I_p} _ mulg.
+Proof. by move=> u v; apply: val_inj; rewrite /= GRing.mulrC. Qed.
+
+Lemma unit_Zp_expg (u : {unit 'I_p}) n :
+  val (u ^+ n) = inZp (val u ^ n) :> 'I_p.
+Proof.
+apply: val_inj => /=; elim: n => [|n IHn] //.
+by rewrite expgS /= IHn expnS modnMmr.
+Qed.
+
+End ZpRing.
+
+Definition Zp_trunc p := p.-2.
+
+Notation "''Z_' p" := 'I_(Zp_trunc p).+2
+  (at level 8, p at level 2, format "''Z_' p") : type_scope.
+Notation "''F_' p" := 'Z_(pdiv p)
+  (at level 8, p at level 2, format "''F_' p") : type_scope.
+
+Section Groups.
+
+Variable p : nat.
+
+Definition Zp := if p > 1 then [set: 'Z_p] else 1%g.
+Definition units_Zp := [set: {unit 'Z_p}].
+
+Lemma Zp_cast : p > 1 -> (Zp_trunc p).+2 = p.
+Proof. by case: p => [|[]]. Qed.
+
+Lemma val_Zp_nat (p_gt1 : p > 1) n : (n%:R : 'Z_p) = (n %% p)%N :> nat.
+Proof. by rewrite Zp_nat /= Zp_cast. Qed.
+
+Lemma Zp_nat_mod (p_gt1 : p > 1)m : (m %% p)%:R = m%:R :> 'Z_p.
+Proof. by apply: ord_inj; rewrite !val_Zp_nat // modn_mod. Qed.
+
+Lemma char_Zp : p > 1 -> p%:R = 0 :> 'Z_p.
+Proof. by move=> p_gt1; rewrite -Zp_nat_mod ?modnn. Qed.
+
+Lemma unitZpE x : p > 1 -> ((x%:R : 'Z_p) \is a GRing.unit) = coprime p x.
+Proof.
+by move=> p_gt1; rewrite qualifE /= val_Zp_nat ?Zp_cast ?coprime_modr.
+Qed.
+
+Lemma Zp_group_set : group_set Zp.
+Proof. rewrite /Zp; case: (p > 1); exact: groupP. Qed.
+Canonical Zp_group := Group Zp_group_set.
+
+Lemma card_Zp : p > 0 -> #|Zp| = p.
+Proof.
+rewrite /Zp; case: p => [|[|p']] //= _; first by rewrite cards1.
+by rewrite cardsT card_ord.
+Qed.
+
+Lemma mem_Zp x : p > 1 -> x \in Zp. Proof. by rewrite /Zp => ->. Qed.
+
+Canonical units_Zp_group := [group of units_Zp].
+
+Lemma card_units_Zp : p > 0 -> #|units_Zp| = totient p.
+Proof.
+move=> p_gt0; transitivity (totient p.-2.+2); last by case: p p_gt0 => [|[|p']].
+rewrite cardsT card_sub -sum1_card big_mkcond /=.
+by rewrite totient_count_coprime big_mkord.
+Qed.
+
+Lemma units_Zp_abelian : abelian units_Zp.
+Proof. apply/centsP=> u _ v _; exact: unit_Zp_mulgC. Qed.
+
+End Groups.
+
+(* Field structure for primes. *)
+
+Section PrimeField.
+
+Open Scope ring_scope.
+
+Variable p : nat.
+
+Section F_prime.
+
+Hypothesis p_pr : prime p.
+
+Lemma Fp_Zcast : (Zp_trunc (pdiv p)).+2 = (Zp_trunc p).+2.
+Proof. by rewrite /pdiv primes_prime. Qed.
+
+Lemma Fp_cast : (Zp_trunc (pdiv p)).+2 = p.
+Proof. by rewrite Fp_Zcast ?Zp_cast ?prime_gt1. Qed.
+
+Lemma card_Fp : #|'F_p| = p.
+Proof. by rewrite card_ord Fp_cast. Qed.
+
+Lemma val_Fp_nat n : (n%:R : 'F_p) = (n %% p)%N :> nat.
+Proof. by rewrite Zp_nat /= Fp_cast. Qed.
+
+Lemma Fp_nat_mod m : (m %% p)%:R = m%:R :> 'F_p.
+Proof. by apply: ord_inj; rewrite !val_Fp_nat // modn_mod. Qed.
+
+Lemma char_Fp : p \in [char 'F_p].
+Proof. by rewrite !inE -Fp_nat_mod p_pr ?modnn. Qed.
+
+Lemma char_Fp_0 : p%:R = 0 :> 'F_p.
+Proof. exact: GRing.charf0 char_Fp. Qed.
+
+Lemma unitFpE x : ((x%:R : 'F_p) \is a GRing.unit) = coprime p x.
+Proof. by rewrite pdiv_id // unitZpE // prime_gt1. Qed.
+
+End F_prime.
+
+Lemma Fp_fieldMixin : GRing.Field.mixin_of [the unitRingType of 'F_p].
+Proof.
+move=> x nzx; rewrite qualifE /= prime_coprime ?gtnNdvd ?lt0n //.
+case: (ltnP 1 p) => [lt1p | ]; last by case: p => [|[|p']].
+by rewrite Zp_cast ?prime_gt1 ?pdiv_prime.
+Qed.
+
+Definition Fp_idomainMixin := FieldIdomainMixin Fp_fieldMixin.
+
+Canonical Fp_idomainType := Eval hnf in IdomainType 'F_p  Fp_idomainMixin.
+Canonical Fp_finIdomainType := Eval hnf in [finIdomainType of 'F_p].
+Canonical Fp_fieldType := Eval hnf in FieldType 'F_p Fp_fieldMixin.
+Canonical Fp_finFieldType := Eval hnf in [finFieldType of 'F_p].
+Canonical Fp_decFieldType :=
+  Eval hnf in [decFieldType of 'F_p for Fp_finFieldType].
+
+End PrimeField.