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, 51 insertions, 1229 deletions

diff --git a/mathcomp/fingroup/AUTHORS b/mathcomp/fingroup/AUTHORS
new file mode 120000
index 0000000..b55a98d
--- /dev/null
+++ b/mathcomp/fingroup/AUTHORS
@@ -0,0 +1 @@
+../../etc/AUTHORS
\ No newline at end of file
diff --git a/mathcomp/fingroup/CeCILL-B b/mathcomp/fingroup/CeCILL-B
new file mode 120000
index 0000000..83e22fd
--- /dev/null
+++ b/mathcomp/fingroup/CeCILL-B
@@ -0,0 +1 @@
+../../etc/CeCILL-B
\ No newline at end of file
diff --git a/mathcomp/fingroup/INSTALL b/mathcomp/fingroup/INSTALL
new file mode 120000
index 0000000..6aa7ec5
--- /dev/null
+++ b/mathcomp/fingroup/INSTALL
@@ -0,0 +1 @@
+../../etc/INSTALL
\ No newline at end of file
diff --git a/mathcomp/fingroup/Make b/mathcomp/fingroup/Make
new file mode 100644
index 0000000..ece5714
--- /dev/null
+++ b/mathcomp/fingroup/Make
@@ -0,0 +1,11 @@
+action.v
+all.v
+automorphism.v
+fingroup.v
+gproduct.v
+morphism.v
+perm.v
+presentation.v
+quotient.v
+
+-R . mathcomp.fingroup
diff --git a/mathcomp/fingroup/Makefile b/mathcomp/fingroup/Makefile
new file mode 100644
index 0000000..d693257
--- /dev/null
+++ b/mathcomp/fingroup/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/fingroup/README b/mathcomp/fingroup/README
new file mode 120000
index 0000000..e4e30e8
--- /dev/null
+++ b/mathcomp/fingroup/README
@@ -0,0 +1 @@
+../../etc/README
\ No newline at end of file
diff --git a/mathcomp/fingroup/all.v b/mathcomp/fingroup/all.v
index 0cf8995..903da3c 100644
--- a/mathcomp/fingroup/all.v
+++ b/mathcomp/fingroup/all.v
@@ -1,10 +1,9 @@
 Require Export action.
 Require Export automorphism.
-Require Export cyclic.
 Require Export fingroup.
 Require Export gproduct.
 Require Export morphism.
 Require Export perm.
 Require Export presentation.
 Require Export quotient.
-Require Export zmodp.
+
diff --git a/mathcomp/fingroup/cyclic.v b/mathcomp/fingroup/cyclic.v
deleted file mode 100644
index ad10492..0000000
--- a/mathcomp/fingroup/cyclic.v
+++ /dev/null
@@ -1,865 +0,0 @@
-(* (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/fingroup/opam b/mathcomp/fingroup/opam
new file mode 100644
index 0000000..4a46943
--- /dev/null
+++ b/mathcomp/fingroup/opam
@@ -0,0 +1,12 @@
+opam-version: "1.2"
+name: "coq:mathcomp:fingroup"
+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/fingroup'" ]
+depends: [ "coq:mathcomp:discrete" { = "1.5" } ]
diff --git a/mathcomp/fingroup/zmodp.v b/mathcomp/fingroup/zmodp.v
deleted file mode 100644
index df5b378..0000000
--- a/mathcomp/fingroup/zmodp.v
+++ /dev/null
@@ -1,362 +0,0 @@
-(* (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.