Updating files + reorganizing everything

12 files changed, 114 insertions, 120 deletions

diff --git a/mathcomp/field/Make b/mathcomp/field/Make
index 6ff83ec..66b6d6a 100644
--- a/mathcomp/field/Make
+++ b/mathcomp/field/Make
@@ -1,4 +1,4 @@
-all.v
+all_field.v
 algC.v
 algebraics_fundamentals.v
 algnum.v
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index 511d69e..a9d1258 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -1,12 +1,13 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-From mathcomp.discrete
-Require Import path div choice fintype bigop finset prime generic_quotient.
-From mathcomp.algebra
-Require Import ssralg poly polydiv mxpoly ssrnum ssrint rat intdiv.
-Require Import countalg algebraics_fundamentals.
+From mathcomp
+Require Import ssrbool ssrfun ssrnat eqtype seq choice div fintype.
+From mathcomp
+Require Import path bigop finset prime ssralg poly polydiv mxpoly.
+From mathcomp
+Require Import generic_quotient countalg ssrnum ssrint rat intdiv.
+From mathcomp
+Require Import algebraics_fundamentals.
 
 (******************************************************************************)
 (* This file provides an axiomatic construction of the algebraic numbers.     *)
@@ -69,7 +70,7 @@ have nz2: 2%:R != 0 :> L.
   apply/eqP=> char2; apply: conj_nt => e; apply/eqP/idPn=> eJ.
   have opp_id x: - x = x :> L.
     by apply/esym/eqP; rewrite -addr_eq0 -mulr2n -mulr_natl char2 mul0r.
-  have{char2} char2: 2 \in [char L] by exact/eqP.
+  have{char2} char2: 2 \in [char L] by apply/eqP.
   without loss{eJ} eJ: e / conj e = e + 1.
     move/(_ (e / (e + conj e))); apply.
     rewrite fmorph_div rmorphD conjK -{1}[conj e](addNKr e) mulrDl.
@@ -1082,7 +1083,7 @@ Proof. by move/(rootCX 0)/(_ ler01). Qed.
 
 Lemma rootCpX n x k : (k > 0)%N -> 0 <= x -> n.-root (x ^+ k) = n.-root x ^+ k.
 Proof.
-by case: n => [|n] k_gt0; [rewrite !root0C expr0n gtn_eqF | exact: rootCX].
+by case: n => [|n] k_gt0; [rewrite !root0C expr0n gtn_eqF | apply: rootCX].
 Qed.
 
 Lemma rootCV n x : (n > 0)%N -> 0 <= x -> n.-root x^-1 = (n.-root x)^-1.
@@ -1253,7 +1254,7 @@ Lemma normC_sum_upper (I : finType) (P : pred I) (F G : I -> algC) :
    forall i, P i -> F i = G i.
 Proof.
 set sumF := \sum_(i | _) _; set sumG := \sum_(i | _) _ => leFG eq_sumFG.
-have posG i: P i -> 0 <= G i by move/leFG; apply: ler_trans; exact: normr_ge0.
+have posG i: P i -> 0 <= G i by move/leFG; apply: ler_trans; apply: normr_ge0.
 have norm_sumG: `|sumG| = sumG by rewrite ger0_norm ?sumr_ge0.
 have norm_sumF: `|sumF| = \sum_(i | P i) `|F i|.
   apply/eqP; rewrite eqr_le ler_norm_sum eq_sumFG norm_sumG -subr_ge0 -sumrB.
@@ -1655,7 +1656,9 @@ Proof. by rewrite !(addrC x) eqCmodDr. Qed.
 
 Lemma eqCmodD e x1 x2 y1 y2 :
   (x1 == x2 %[mod e] -> y1 == y2 %[mod e] -> x1 + y1 == x2 + y2 %[mod e])%C.
-Proof. rewrite -(eqCmodDl e x2 y1) -(eqCmodDr e y1); exact: eqCmod_trans. Qed.
+Proof.
+by rewrite -(eqCmodDl e x2 y1) -(eqCmodDr e y1); apply: eqCmod_trans.
+Qed.
 
 Lemma eqCmod_nat (e m n : nat) : (m == n %[mod e])%C = (m == n %[mod e]).
 Proof.
@@ -1832,7 +1835,7 @@ Section AutLmodC.
 Variables (U V : lmodType algC) (f : {additive U -> V}).
 
 Lemma raddfZ_Cnat a u : a \in Cnat -> f (a *: u) = a *: f u. 
-Proof. by case/CnatP=> n ->; exact: raddfZnat. Qed.
+Proof. by case/CnatP=> n ->; apply: raddfZnat. Qed.
 
 Lemma raddfZ_Cint a u : a \in Cint -> f (a *: u) = a *: f u. 
 Proof. by case/CintP=> m ->; rewrite !scaler_int raddfMz. Qed.
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 7381b82..f72f67e 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -1,18 +1,15 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-From mathcomp.discrete
-Require Import div path choice fintype tuple bigop finset prime.
-From mathcomp.fingroup
-Require Import fingroup.
-From mathcomp.algebra
-Require Import ssralg poly polydiv mxpoly finalg zmodp cyclic.
-From mathcomp.algebra
-Require Import ssrnum ssrint rat intdiv vector.
-From mathcomp.solvable
-Require Import pgroup sylow.
-Require Import countalg falgebra fieldext separable galois.
+From mathcomp
+Require Import ssrbool ssrfun ssrnat eqtype seq choice div fintype.
+From mathcomp
+Require Import path tuple bigop finset prime ssralg poly polydiv mxpoly.
+From mathcomp
+Require Import countalg ssrnum ssrint rat intdiv.
+From mathcomp
+Require Import fingroup finalg zmodp cyclic pgroup sylow.
+From mathcomp
+Require Import vector falgebra fieldext separable galois.
 
 (******************************************************************************)
 (*   The main result in this file is the existence theorem that underpins the *)
diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
index cddc383..1dd7fb9 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -1,14 +1,13 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-From mathcomp.discrete
-Require Import path div choice fintype tuple finfun bigop prime.
-From mathcomp.algebra
-Require Import ssralg finalg zmodp poly ssrnum ssrint rat polydiv intdiv.
-From mathcomp.algebra
-Require Import matrix mxalgebra mxpoly vector.
-Require Import algC falgebra fieldext separable galois cyclotomic.
+From mathcomp
+Require Import ssrbool ssrfun eqtype ssrnat seq path div choice.
+From mathcomp
+Require Import fintype tuple finfun bigop prime ssralg finalg zmodp poly.
+From mathcomp
+Require Import ssrnum ssrint rat polydiv intdiv algC matrix mxalgebra mxpoly.
+From mathcomp
+Require Import vector falgebra fieldext separable galois cyclotomic.
 
 (******************************************************************************)
 (* This file provides a few basic results and constructions in algebraic      *)
@@ -81,7 +80,7 @@ suffices /sig_eqW[[n [|px [|pz []]]]// [Dpx Dpz]]:
   by rewrite map_comp_poly horner_comp -Dpz.
 have [rx nz_rx rx0] := r_exists x.
 have [rz nz_rz rz0] := r_exists (- z).
-have char0_Q: [char rat] =i pred0 by exact: char_num.
+have char0_Q: [char rat] =i pred0 by apply: char_num.
 have [n [[pz Dpz] [px Dpx]]] := char0_PET nz_rz rz0 nz_rx rx0 char0_Q.
 by exists (n, [:: px; - pz]); rewrite /= !raddfN hornerN -[z]opprK Dpz Dpx.
 Qed.
@@ -197,7 +196,7 @@ by rewrite mulr_sumr; apply: eq_bigr => i _; rewrite ffunE mulrA -rmorphM.
 Qed.
 
 Lemma Crat_spanM b : {in Crat & Crat_span b, forall a x, a * x \in Crat_span b}.
-Proof. by move=> _ x /CratP[a ->]; exact: Crat_spanZ. Qed.
+Proof. by move=> _ x /CratP[a ->]; apply: Crat_spanZ. Qed.
 
 (* In principle CtoQn could be taken to be additive and Q-linear, but this    *)
 (* would require a limit construction.                                        *)
@@ -234,7 +233,7 @@ Lemma map_Qnum_poly (nu : {rmorphism algC -> algC}) p :
   p \in polyOver 1%VS -> map_poly (nu \o QnC) p = (map_poly QnC p).
 Proof.
 move=> Qp; apply/polyP=> i; rewrite /= !coef_map /=.
-have /vlineP[a ->]: p`_i \in 1%VS by exact: polyOverP.
+have /vlineP[a ->]: p`_i \in 1%VS by apply: polyOverP.
 by rewrite alg_num_field !fmorph_rat.
 Qed.
 
@@ -483,7 +482,7 @@ have pzn_zk0: root (map_poly \1%VF (minPoly 1 zn)) (zn ^+ k).
   set p1 := map_poly _ _.
   have [q1 Dp1]: exists q1, p1 = pQtoC q1.
     have aP i: (minPoly 1 zn)`_i \in 1%VS.
-      by apply/polyOverP; exact: minPolyOver.
+      by apply/polyOverP; apply: minPolyOver.
     have{aP} a_ i := sig_eqW (vlineP _ _ (aP i)).
     exists (\poly_(i < size (minPoly 1 zn)) sval (a_ i)).
     apply/polyP=> i; rewrite coef_poly coef_map coef_poly /=.
@@ -584,7 +583,7 @@ have IY_0: 0 \in IY by apply/familyP=> // i; rewrite ffunE.
 pose inIY := enum_rank_in IY_0.
 pose Y := [seq \prod_(i < m) X`_i ^+ (f : 'I_N ^ m) i | f in IY].
 have S_P := Cint_spanP [tuple of Y]; set S := Cint_span _ in S_P.
-have sYS: {subset Y <= S} by exact: mem_Cint_span.
+have sYS: {subset Y <= S} by apply: mem_Cint_span.
 have S_1: 1 \in S.
   by apply/sYS/imageP; exists 0 => //; rewrite big1 // => i; rewrite ffunE.
 have SmulX (i : 'I_m): {in S, forall x, x * X`_i \in S}.
@@ -596,7 +595,7 @@ have SmulX (i : 'I_m): {in S, forall x, x * X`_i \in S}.
       by rewrite inordK // ltnS (bigmax_sup i).
     exists (finfun [eta f with i |-> inord (f i).+1]).
       apply/familyP=> i1; rewrite inE ffunE /= fun_if fiK.
-      by case: eqP => [-> // | _]; exact: fP.
+      by case: eqP => [-> // | _]; apply: fP.
     rewrite (bigD1 i isT) ffunE /= eqxx fiK; congr (_ * _).
     by apply: eq_bigr => i1; rewrite ffunE /= => /negPf->.
   have [/monicP ] := (minCpoly_monic X`_i, root_minCpoly X`_i).
@@ -609,7 +608,7 @@ have SmulX (i : 'I_m): {in S, forall x, x * X`_i \in S}.
   have eK: (inord e : 'I_N) = e :> nat by rewrite inordK // ltnS (bigmax_sup i).
   exists (finfun [eta f with i |-> inord e]).
     apply/familyP=> i1; rewrite inE ffunE /= fun_if eK.
-    by case: eqP => [-> // | _]; exact: fP.
+    by case: eqP => [-> // | _]; apply: fP.
   rewrite (bigD1 i isT) ffunE /= eqxx eK; congr (_ * _).
   by apply: eq_bigr => i1; rewrite ffunE /= => /negPf->.
 exists S; last by exists (Tagged (fun n => n.-tuple _) [tuple of Y]).
@@ -733,7 +732,9 @@ Proof. by rewrite !(addrC x) eqAmodDr. Qed.
 
 Lemma eqAmodD e x1 x2 y1 y2 :
   (x1 == x2 %[mod e] -> y1 == y2 %[mod e] -> x1 + y1 == x2 + y2 %[mod e])%A.
-Proof. rewrite -(eqAmodDl e x2 y1) -(eqAmodDr e y1); exact: eqAmod_trans. Qed.
+Proof.
+by rewrite -(eqAmodDl e x2 y1) -(eqAmodDr e y1); apply: eqAmod_trans.
+Qed.
 
 Lemma eqAmodm0 e : (e == 0 %[mod e])%A.
 Proof. by rewrite /eqAmod subr0 unfold_in; case: ifPn => // /divff->. Qed.
diff --git a/mathcomp/field/all.v b/mathcomp/field/all_field.v
index c26dbba..c26dbba 100644
--- a/mathcomp/field/all.v
+++ b/mathcomp/field/all_field.v
diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v
index b96fc38..94df28b 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -1,11 +1,9 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-From mathcomp.discrete
-Require Import bigop.
-From mathcomp.algebra
-Require Import ssralg poly polydiv.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat seq.
+From mathcomp
+Require Import bigop ssralg poly polydiv.
 
 (******************************************************************************)
 (*   A proof that algebraically closed field enjoy quantifier elimination,    *)
@@ -313,7 +311,7 @@ Lemma redivpT_qf (p : polyF) (k : nat * polyF * polyF -> formula F) (q : polyF)
 Proof.
 move=> kP rp rq; rewrite /redivpT; apply: isnull_qf=> // [[]]; first exact: kP.
 apply: sizeT_qf => // sq; apply: sizeT_qf=> // sp.
-apply: lead_coefT_qf=> // lq rlq; exact: redivp_rec_loopT_qf.
+by apply: lead_coefT_qf=> // lq rlq; apply: redivp_rec_loopT_qf.
 Qed.
 
 Definition rmodpT (p : polyF) (k : polyF -> fF) (q : polyF) : fF :=
@@ -603,7 +601,7 @@ rewrite -!map_comp.
     \big[(@gcdp F)/0]_(j <- l) P j %= \big[(@rgcdp F)/0]_(j <- l) P j.
     elim: l => [| u l ihl] /=; first by rewrite !big_nil eqpxx.
     rewrite !big_cons; move: ihl; move/(eqp_gcdr (P u)) => h.
-    apply: eqp_trans h _; rewrite eqp_sym; exact: eqp_rgcd_gcd.
+    by apply: eqp_trans h _; rewrite eqp_sym; apply: eqp_rgcd_gcd.
 case g0: (\big[(@rgcdp F)/0%:P]_(j <- map (eval_poly e \o abstrX i) ps) j == 0).
   rewrite (eqP g0) rgdcop0.
   case m0 : (_ == 0)=> //=; rewrite ?(size_poly1,size_poly0) //=.
diff --git a/mathcomp/field/countalg.v b/mathcomp/field/countalg.v
index de6f01e..dfac24b 100644
--- a/mathcomp/field/countalg.v
+++ b/mathcomp/field/countalg.v
@@ -1,14 +1,13 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-From mathcomp.discrete
-Require Import choice fintype bigop generic_quotient.
-From mathcomp.algebra
-Require Import ssralg finalg zmodp matrix mxalgebra poly polydiv mxpoly.
-From mathcomp.algebra
-Require Import ring_quotient ssrint rat mxpoly polyXY.
-Require Import closed_field.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
+From mathcomp
+Require Import bigop ssralg finalg zmodp matrix mxalgebra.
+From mathcomp
+Require Import poly polydiv mxpoly generic_quotient ring_quotient closed_field.
+From mathcomp
+Require Import ssrint rat.
 
 (*****************************************************************************)
 (* This file clones part of ssralg hierachy for countable types; it does not *)
@@ -800,7 +799,13 @@ Export Zmodule.Exports Ring.Exports ComRing.Exports UnitRing.Exports.
 Export ComUnitRing.Exports IntegralDomain.Exports.
 Export Field.Exports DecidableField.Exports ClosedField.Exports.
 
+From mathcomp
+Require Import poly polydiv generic_quotient ring_quotient.
+From mathcomp
+Require Import mxpoly polyXY.
 Import GRing.Theory.
+From mathcomp
+Require Import closed_field.
 
 Canonical Zp_countZmodType m := [countZmodType of 'I_m.+1].
 Canonical Zp_countRingType m := [countRingType of 'I_m.+2].
@@ -915,7 +920,7 @@ have EmulV: GRing.Field.axiom Einv.
     by rewrite piE -{1}[z]reprK -Quotient.idealrBE subr0 in nz_z.
   apply/eqP; case: sig_eqW => {ex_uv} [uv uv1]; set i := _.+1 in uv1 *.
   rewrite piE /= -[z]reprK -(rmorphM PtoE) -Quotient.idealrBE.
-  by rewrite -uv1 opprD addNKr -mulNr; apply/memI; exists i; exact: dvdp_mull.
+  by rewrite -uv1 opprD addNKr -mulNr; apply/memI; exists i; apply: dvdp_mull.
 pose EringU := [comUnitRingType of UnitRingType _ (FieldUnitMixin EmulV Einv0)].
 have Eunitf := @FieldMixin _ _ EmulV Einv0.
 pose Efield := FieldType (IdomainType EringU (FieldIdomainMixin Eunitf)) Eunitf.
diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v
index 39faf38..8080dd3 100644
--- a/mathcomp/field/cyclotomic.v
+++ b/mathcomp/field/cyclotomic.v
@@ -1,16 +1,15 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-From mathcomp.discrete
-Require Import div path choice fintype tuple finfun bigop finset prime.
-From mathcomp.fingroup
-Require Import fingroup.
-From mathcomp.algebra
-Require Import ssralg poly finalg zmodp cyclic.
-From mathcomp.algebra
-Require Import ssrnum ssrint polydiv rat intdiv mxpoly vector.
-Require Import falgebra fieldext separable galois algC.
+From mathcomp
+Require Import ssrbool ssrfun eqtype ssrnat seq path div choice.
+From mathcomp
+Require Import fintype tuple finfun bigop prime ssralg poly finset.
+From mathcomp
+Require Import fingroup finalg zmodp cyclic.
+From mathcomp
+Require Import ssrnum ssrint polydiv rat intdiv.
+From mathcomp
+Require Import mxpoly vector falgebra fieldext separable galois algC.
 
 (******************************************************************************)
 (* This file provides few basic properties of cyclotomic polynomials.         *)
@@ -160,7 +159,7 @@ rewrite /'Phi_n; case: (C_prim_root_exists _) => z /=.
 have n_gt0 := prim_order_gt0 prim_z0; rewrite prednK // => prim_z.
 have [uDn _ inDn] := divisors_correct n_gt0.
 pose q := \prod_(d <- rem n (divisors n)) 'Phi_d.
-have mon_q: q \is monic by apply: monic_prod => d _; exact: Cyclotomic_monic.
+have mon_q: q \is monic by apply: monic_prod => d _; apply: Cyclotomic_monic.
 have defXn1: cyclotomic z n * pZtoC q = 'X^n - 1.
   rewrite (prod_cyclotomic prim_z) (big_rem n) ?inDn //=.
   rewrite divnn n_gt0 rmorph_prod /=; congr (_ * _).
@@ -229,7 +228,7 @@ Lemma minCpoly_cyclotomic n z :
 Proof.
 move=> prim_z; have n_gt0 := prim_order_gt0 prim_z.
 have Dpz := Cintr_Cyclotomic prim_z; set pz := cyclotomic z n in Dpz *.
-have mon_pz: pz \is monic by exact: cyclotomic_monic.
+have mon_pz: pz \is monic by apply: cyclotomic_monic.
 have pz0: root pz z by rewrite root_cyclotomic.
 have [pf [Dpf mon_pf] dv_pf] := minCpolyP z.
 have /dvdpP_rat_int[f [af nz_af Df] [g /esym Dfg]]: pf %| pZtoQ 'Phi_n.
diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v
index ba96824..32acb2c 100644
--- a/mathcomp/field/falgebra.v
+++ b/mathcomp/field/falgebra.v
@@ -1,11 +1,9 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-From mathcomp.discrete
-Require Import path div choice fintype tuple finfun bigop.
-From mathcomp.algebra
-Require Import ssralg finalg zmodp matrix vector poly.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat seq path choice fintype.
+From mathcomp
+Require Import div tuple finfun bigop ssralg finalg zmodp matrix vector poly.
 
 (******************************************************************************)
 (* Finite dimensional free algebras, usually known as F-algebras.             *)
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index 8ec0943..6d63965 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -1,14 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-From mathcomp.discrete
-Require Import div choice fintype tuple finfun bigop generic_quotient.
-From mathcomp.algebra
-Require Import ssralg finalg zmodp matrix vector poly polydiv mxpoly.
-Require Import falgebra.
-
-
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat seq div choice fintype.
+From mathcomp
+Require Import tuple finfun bigop ssralg finalg zmodp matrix vector falgebra.
+From mathcomp
+Require Import poly polydiv mxpoly generic_quotient.
 
 (******************************************************************************)
 (*  * Finite dimensional field extentions                                     *)
@@ -847,9 +844,9 @@ have v2rP x: {r : 'rV[K_F]_n | x = r2v r}.
 pose v2r x := sval (v2rP x).
 have v2rK: cancel v2r (Linear r2v_lin) by rewrite /v2r => x; case: (v2rP x).
 suffices r2vK: cancel r2v v2r.
-  by exists n, v2r; [exact: can2_linear v2rK | exists r2v].
+  by exists n, v2r; [apply: can2_linear v2rK | exists r2v].
 move=> r; apply/rowP=> i; apply/val_inj/(mulIf (nz_bLi i))/eqP; move: i isT.
-by apply/forall_inP; move/directv_sum_unique: dxSbL => <- //; exact/eqP/v2rK.
+by apply/forall_inP; move/directv_sum_unique: dxSbL => <- //; apply/eqP/v2rK.
 Qed.
 
 Canonical fieldOver_vectType := VectType K_F L_F fieldOver_vectMixin.
@@ -885,7 +882,7 @@ Qed.
 Fact aspaceOver_suproof E : is_aspace (vspaceOver E).
 Proof.
 rewrite /is_aspace has_algid1; last by rewrite mem_vspaceOver (@mem1v _ L).
-by apply/prodvP=> u v; rewrite !mem_vspaceOver; exact: memvM.
+by apply/prodvP=> u v; rewrite !mem_vspaceOver; apply: memvM.
 Qed.
 Canonical aspaceOver E := ASpace (aspaceOver_suproof E).
 
@@ -907,7 +904,7 @@ by rewrite scaler_eq0=> /predU1P[] // /idPn[]; rewrite (memPn nz_b) ?memt_nth.
 Qed.
 
 Lemma dim_aspaceOver E : (F <= E)%VS -> \dim (vspaceOver E) = \dim_F E.
-Proof. by rewrite -sup_field_module; exact: dim_vspaceOver. Qed.
+Proof. by rewrite -sup_field_module; apply: dim_vspaceOver. Qed.
 
 Lemma vspaceOverP V_F :
   {V | [/\ V_F = vspaceOver V, (F * V <= V)%VS & V_F =i V]}.
@@ -932,8 +929,8 @@ Proof.
 have [V [defEF modV memV]] := vspaceOverP E_F.
 have algE: has_algid V && (V * V <= V)%VS.
   rewrite has_algid1; last by rewrite -memV mem1v.
-  by apply/prodvP=> u v; rewrite -!memV; exact: memvM.
-by exists (ASpace algE); rewrite -sup_field_module; split; first exact: val_inj.
+  by apply/prodvP=> u v; rewrite -!memV; apply: memvM.
+by exists (ASpace algE); rewrite -sup_field_module; split; first apply: val_inj.
 Qed.
 
 End FieldOver.
@@ -1057,7 +1054,7 @@ Qed.
 Fact baseAspace_suproof (E : {subfield L}) : is_aspace (baseVspace E).
 Proof.
 rewrite /is_aspace has_algid1; last by rewrite mem_baseVspace (mem1v E).
-by apply/prodvP=> u v; rewrite !mem_baseVspace; exact: memvM.
+by apply/prodvP=> u v; rewrite !mem_baseVspace; apply: memvM.
 Qed.
 Canonical baseAspace E := ASpace (baseAspace_suproof E).
 
@@ -1072,7 +1069,7 @@ Proof. by rewrite [F1]unlock dim_baseVspace dimv1 mul1n. Qed.
 Lemma baseVspace_module V (V0 := baseVspace V) : (F1 * V0 <= V0)%VS.
 Proof.
 apply/prodvP=> u v; rewrite [F1]unlock !mem_baseVspace => /vlineP[x ->] Vv.
-by rewrite -(@scalerAl F L) mul1r; exact: memvZ.
+by rewrite -(@scalerAl F L) mul1r; apply: memvZ.
 Qed.
 
 Lemma sub_baseField (E : {subfield L}) : (F1 <= baseVspace E)%VS.
@@ -1106,7 +1103,7 @@ Lemma module_baseAspace (E0 : {subfield L0}) :
   (F1 <= E0)%VS -> {E | E0 = baseAspace E & E0 =i E}.
 Proof.
 rewrite -sup_field_module => /module_baseVspace[E defE0 memE0].
-suffices algE: is_aspace E by exists (ASpace algE); first exact: val_inj.
+suffices algE: is_aspace E by exists (ASpace algE); first apply: val_inj.
 rewrite /is_aspace has_algid1 -?memE0 ?mem1v //.
 by apply/prodvP=> u v; rewrite -!memE0; apply: memvM.
 Qed.
@@ -1387,7 +1384,7 @@ Proof. by rewrite /subfx_scale rmorphM mulrA. Qed.
 Fact subfx_scaler1r : left_id 1 subfx_scale.
 Proof. by move=> x; rewrite /subfx_scale rmorph1 mul1r. Qed.
 Fact subfx_scalerDr : right_distributive subfx_scale +%R.
-Proof. by move=> a; exact: mulrDr. Qed.
+Proof. by move=> a; apply: mulrDr. Qed.
 Fact subfx_scalerDl x : {morph subfx_scale^~ x : a b / a + b}.
 Proof. by move=> a b; rewrite /subfx_scale rmorphD mulrDl. Qed.
 Definition subfx_lmodMixin :=
@@ -1606,7 +1603,7 @@ have unitE: GRing.Field.mixin_of urL.
   have nz_q: q != 0 by rewrite -(can_eq (@rVpolyK _ _)) raddf0 in nz_x.
   have /Bezout_eq1_coprimepP[u upq1]: coprimep p q.
     have /contraR := irr_p _ _ (dvdp_gcdl p q); apply.
-    have: size (gcdp p q) <= size q by exact: leq_gcdpr.
+    have: size (gcdp p q) <= size q by apply: leq_gcdpr.
     rewrite leqNgt;apply:contra;move/eqp_size ->.
     by rewrite (polySpred nz_p) ltnS size_poly.
   suffices: x * toL u.2 = 1 by exists (toL u.2); rewrite mulrC.
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index f0bcb0b..8ad9c8c 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -1,14 +1,13 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-From mathcomp.discrete
-Require Import div choice fintype tuple finfun bigop finset.
-From mathcomp.fingroup
-Require Import fingroup morphism quotient perm action.
-From mathcomp.algebra
-Require Import ssralg poly polydiv zmodp cyclic matrix mxalgebra vector.
-Require Import  falgebra fieldext separable.
+From mathcomp
+Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype.
+From mathcomp
+Require Import tuple finfun bigop ssralg poly polydiv.
+From mathcomp
+Require Import finset fingroup morphism quotient perm action zmodp cyclic.
+From mathcomp
+Require Import matrix mxalgebra vector falgebra fieldext separable.
 
 (******************************************************************************)
 (* This file develops some basic Galois field theory, defining:               *)
diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v
index 40e3f93..ba6e3ce 100644
--- a/mathcomp/field/separable.v
+++ b/mathcomp/field/separable.v
@@ -1,16 +1,13 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-From mathcomp.discrete
-Require Import div choice fintype tuple finfun bigop prime finset binomial.
-From mathcomp.fingroup
-Require Import fingroup morphism perm  quotient action gproduct.
-From mathcomp.algebra
-Require Import ssralg poly polydiv finalg zmodp cyclic matrix mxalgebra mxpoly.
-From mathcomp.algebra
-Require Import matrix mxalgebra mxpoly polyXY vector.
-Require Import falgebra fieldext.
+From mathcomp
+Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype.
+From mathcomp
+Require Import tuple finfun bigop finset prime binomial ssralg poly polydiv.
+From mathcomp
+Require Import fingroup perm morphism quotient gproduct finalg zmodp cyclic.
+From mathcomp
+Require Import matrix mxalgebra mxpoly polyXY vector falgebra fieldext.
 
 (******************************************************************************)
 (* This file provides a theory of separable and inseparable field extensions. *)