running semi-automated linting on the whole library

9 files changed, 68 insertions, 66 deletions

diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index 2e8ce3f..b045c07 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -152,7 +152,7 @@ have sposDl x y : lt 0 x -> le 0 y -> lt 0 (x + y).
   have sqrtJ z : le 0 z -> conj (sqrt z) = sqrt z.
     rewrite posE -{2}[z]sqrtK -subr_eq0 -mulrBr mulf_eq0 subr_eq0.
     by case/pred2P=> ->; rewrite ?rmorph0.
-  case/andP=> nz_x /sqrtJ uJ /sqrtJ vJ. 
+  case/andP=> nz_x /sqrtJ uJ /sqrtJ vJ.
   set u := sqrt x in uJ; set v := sqrt y in vJ; pose w := u + i * v.
   have ->: x + y = w * conj w.
     rewrite rmorphD rmorphM iJ uJ vJ mulNr mulrC -subr_sqr sqrMi opprK.
@@ -171,7 +171,7 @@ have normD x y : le (norm (x + y)) (norm x + norm y).
     by have /andP[]: lt 0 (u + v) by rewrite sposDl // /lt nz_u.
   have le_sqr u v: conj u = u -> le 0 v -> le (u ^+ 2) (v ^+ 2) -> le u v.
     move=> Ru v_ge0; have [-> // | nz_u] := eqVneq u 0.
-    have [u_gt0 | u_le0 _] := boolP (lt 0 u).    
+    have [u_gt0 | u_le0 _] := boolP (lt 0 u).
       by rewrite leB (leB u) subr_sqr mulrC addrC; apply: sposM; apply: sposDl.
     rewrite leB posD // posE normN -addr_eq0; apply/eqP.
     rewrite /lt nz_u posE -subr_eq0 in u_le0; apply: (mulfI u_le0).
@@ -184,7 +184,7 @@ have normD x y : le (norm (x + y)) (norm x + norm y).
     by rewrite rmorphD !rmorphM !conjK addrC mulrC (mulrC y).
   rewrite -mulr2n -mulr_natr exprMn normK -natrX mulr_natr sqrrD mulrACA.
   rewrite -rmorphM (mulrC y x) addrAC leB mulrnA mulr2n opprD addrACA.
-  rewrite  subrr addr0 {2}(mulrC x) rmorphM mulrACA -opprB addrAC -sqrrB -sqrMi.
+  rewrite subrr addr0 {2}(mulrC x) rmorphM mulrACA -opprB addrAC -sqrrB -sqrMi.
   apply/posP; exists (i * (x * conj y - y * conj x)); congr (_ * _).
   rewrite !(rmorphM, rmorphB) iJ !conjK mulNr -mulrN opprB.
   by rewrite (mulrC x) (mulrC y).
@@ -421,7 +421,7 @@ Lemma conjK : involutive conj.
 Proof. by move=> u; apply: CtoL_inj; rewrite !LtoC_K conjL_K. Qed.
 
 Fact conj_nt : ~ conj =1 id.
-Proof. 
+Proof.
 have [i i2]: exists i : type, i ^+ 2 = -1.
   have [i] := @solve_monicpoly _ 2 (nth 0 [:: -1 : type]) isT.
   by rewrite !big_ord_recl big_ord0 /= mul0r mulr1 !addr0; exists i.
@@ -988,7 +988,7 @@ Proof.
 rewrite unfold_in CintEge0 ?divr_ge0 ?invr_ge0 ?ler0n // !pnatr_eq0.
 have [-> | nz_p] := altP eqP; first by rewrite dvd0n.
 apply/CnatP/dvdnP=> [[q def_q] | [q ->]]; exists q.
-  by apply/eqP; rewrite -eqC_nat natrM -def_q divfK ?pnatr_eq0. 
+  by apply/eqP; rewrite -eqC_nat natrM -def_q divfK ?pnatr_eq0.
 by rewrite [num in num / _]natrM mulfK ?pnatr_eq0.
 Qed.
 
@@ -1213,10 +1213,10 @@ 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. 
+Lemma raddfZ_Cnat a u : a \in Cnat -> f (a *: u) = a *: f u.
 Proof. by case/CnatP=> n ->; apply: raddfZnat. Qed.
 
-Lemma raddfZ_Cint a u : a \in Cint -> f (a *: u) = a *: f u. 
+Lemma raddfZ_Cint a u : a \in Cint -> f (a *: u) = a *: f u.
 Proof. by case/CintP=> m ->; rewrite !scaler_int raddfMz. Qed.
 
 End AutLmodC.
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 405a5d9..891bce5 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -561,7 +561,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}.
     have [m [le_vm le_wm _]] := maxn3 (n_ v) (n_ w) 0%N; rewrite !(posE m) //.
     by rewrite /nlim limN -ltr_normr (ltr_trans e_gt0) ?v_gte ?ab_le.
   have posD v w: lt 0 v -> lt 0 w -> lt 0 (v + w).
-    move=>  /posP[m [d d_gt0 v_gtd]] /posP[n [e e_gt0 w_gte]].
+    move=> /posP[m [d d_gt0 v_gtd]] /posP[n [e e_gt0 w_gte]].
     apply/posP; exists (maxn m n), (d + e) => [|k]; first exact: addr_gt0.
     rewrite geq_max => /andP[le_mk le_nk]; rewrite /nlim /lim.
     have ->: q_ (v + w) = q_ v + q_ w.
diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
index c75bead..fcd6c2d 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -271,7 +271,7 @@ pose z_s := [seq coord b ij.2 (tnth s ij.1) | ij : IzT].
 pose rank2 j i: Iz := enum_rank (i, j); pose val21 (p : Iz) := (enum_val p).1.
 pose inQzs w := [forall j, Crat_span z_s (coord b j w)].
 have enum_pairK j: {in predT, cancel (rank2 j) val21}.
-  by move=> i; rewrite /val21 enum_rankK. 
+  by move=> i; rewrite /val21 enum_rankK.
 have Qz_Zs a: inQzs (\sum_(i < m) s`_i *~ a i).
   apply/forallP=> j; apply/Crat_spanP; rewrite /in_Crat_span size_map -cardE.
   exists [ffun ij => (a (val21 ij))%:Q *+ ((enum_val ij).2 == j)].
diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v
index 8a2e304..05cf477 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -98,9 +98,9 @@ rewrite -cons_poly_def /lift polyseq_cons /nilp.
 case pn0: (_ == _) => /=; last by move->; rewrite -cons_poly_def.
 move=> _; rewrite polyseqC.
 case c0: (_==_)=> /=.
-  move: pn0; rewrite (eqP c0) size_poly_eq0; move/eqP->. 
-  by apply:val_inj=> /=; rewrite polyseq_cons // polyseq0.
-by rewrite mul0r add0r; apply:val_inj=> /=; rewrite polyseq_cons // /nilp pn0.
+  move: pn0; rewrite (eqP c0) size_poly_eq0; move/eqP->.
+  by apply: val_inj=> /=; rewrite polyseq_cons // polyseq0.
+by rewrite mul0r add0r; apply: val_inj=> /=; rewrite polyseq_cons // /nilp pn0.
 Qed.
 
 Fixpoint lead_coefT (k : term F -> fF) p :=  
@@ -181,11 +181,11 @@ Qed.
 
 Lemma rpoly_map_mul (t : term F) (p : polyF) (rt : rterm t) : 
   rpoly (map (Mul t) p) = rpoly p.
-Proof. 
+Proof.
 by rewrite /rpoly all_map /= (@eq_all _ _ (@rterm _)) // => x; rewrite /= rt.
 Qed.
 
-Lemma rmulpT (p q : polyF) : rpoly p -> rpoly q -> rpoly (mulpT p q). 
+Lemma rmulpT (p q : polyF) : rpoly p -> rpoly q -> rpoly (mulpT p q).
 Proof.
 elim: p q=> [|a p ihp] q rp rq //=; move: rp; case/andP=> ra rp /=.
 apply: rsumpT; last exact: ihp.
@@ -206,7 +206,7 @@ Lemma eval_natmulpT  (p : polyF) (n : nat) (e : seq F) :
   eval_poly e (natmulpT n p) = (eval_poly e p) *+ n.
 Proof.
 elim: p; rewrite //= ?mul0rn // => c p ->.
-rewrite mulrnDl mulr_natl polyC_muln; congr (_+_). 
+rewrite mulrnDl mulr_natl polyC_muln; congr (_+_).
 by rewrite -mulr_natl mulrAC -mulrA mulr_natl mulrC.
 Qed.
 
@@ -245,16 +245,16 @@ move=> Pk q sq cq c qq r n e /=.
 elim: n c qq r k Pk e => [|n Pn] c qq r k Pk e; rewrite sizeTP.
   case ltrq : (_ < _); first by rewrite /= ltrq /= -Pk.
   rewrite lead_coefTP => [|a p]; rewrite Pk.
-    rewrite ?(eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT) //=. 
+    rewrite ?(eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT) //=.
     by rewrite ltrq //= mul_polyC ?(mul0r,add0r).
   by symmetry; rewrite Pk ?(eval_mulpT,eval_amulXnT,eval_sumpT, eval_opppT).
 case ltrq : (_<_); first by rewrite /= ltrq Pk.
 rewrite lead_coefTP.
-  rewrite Pn ?(eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT) //=. 
+  rewrite Pn ?(eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT) //=.
   by rewrite ltrq //= mul_polyC ?(mul0r,add0r).
 rewrite -/redivp_rec_loopT => x e'.
-rewrite Pn; last by move=>*; rewrite Pk. 
-symmetry; rewrite Pn; last by move=>*; rewrite Pk.
+rewrite Pn; last by move=> *; rewrite Pk.
+symmetry; rewrite Pn; last by move=> *; rewrite Pk.
 rewrite Pk ?(eval_lift,eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT).
 by rewrite mul_polyC ?(mul0r,add0r).
 Qed.
@@ -267,7 +267,7 @@ Lemma redivp_rec_loopT_qf (q : polyF) (sq : nat) (cq : term F)
 Proof.
 elim: n q sq cq k c qq r => [|n ihn] q sq cq k c qq r kP rq rcq rqq rr.
   apply: sizeT_qf=> // n; case: (_ < _); first by apply: kP; rewrite // rqq rr.
-  apply: lead_coefT_qf=> // l rl; apply: kP. 
+  apply: lead_coefT_qf=> // l rl; apply: kP.
   by rewrite /= ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul) //= rcq.
 apply: sizeT_qf=> // m; case: (_ < _); first by apply: kP => //=; rewrite rqq rr.
 apply: lead_coefT_qf=> // l rl; apply: ihn; rewrite //= ?rcq //.
@@ -290,7 +290,7 @@ Definition redivpT (p : polyF) (k : nat * polyF * polyF -> fF)
 
 Lemma redivp_rec_loopP  (q : {poly F}) (c : nat) (qq r : {poly F}) (n : nat) :
   redivp_rec q c qq r n = redivp_rec_loop q (size q) (lead_coef q) c qq r n.
-Proof. by elim: n c qq r => [| n Pn] c qq r //=; rewrite Pn. Qed. 
+Proof. by elim: n c qq r => [| n Pn] c qq r //=; rewrite Pn. Qed.
 
 Lemma redivpTP (k : nat * polyF * polyF -> formula F) :
   (forall c qq r e,  
@@ -346,12 +346,12 @@ Lemma rgcdp_loopP (k : polyF -> formula F) :
 Proof.
 move=> Pk n p q e.
 elim: n p q e => /= [| m Pm] p q e.
-  rewrite redivpTP; last by move=>*; rewrite !isnullP eval_lift.
+  rewrite redivpTP; last by move=> *; rewrite !isnullP eval_lift.
   rewrite isnullP eval_lift; case: (_ == 0); first by rewrite Pk.
-  by rewrite redivpTP; last by move=>*; rewrite Pk.
-rewrite redivpTP; last by move=>*; rewrite !isnullP eval_lift.
+  by rewrite redivpTP; last by move=> *; rewrite Pk.
+rewrite redivpTP; last by move=> *; rewrite !isnullP eval_lift.
 rewrite isnullP eval_lift; case: (_ == 0); first by rewrite Pk.
-by rewrite redivpTP; move=>*; rewrite ?Pm !eval_lift.
+by rewrite redivpTP => - *; rewrite ?Pm !eval_lift.
 Qed.
 
 Lemma rgcdp_loopT_qf (p : polyF) (k : polyF -> formula F) (q : polyF) (n : nat) :
@@ -371,16 +371,16 @@ Definition rgcdpT (p : polyF) k (q : polyF) : fF :=
     (fun b => if b 
       then (k q1) 
       else (sizeT (fun n => (rgcdp_loopT p1 k n q1)) p1)) p1
-    in (lt_sizeT (fun b => if b then (aux q k p) else (aux p k q)) p q). 
+    in (lt_sizeT (fun b => if b then (aux q k p) else (aux p k q)) p q).
 
 Lemma rgcdpTP (k : seq (term F) -> formula F) :
   (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) ->
    forall p q e, qf_eval e (rgcdpT p k q) = 
                  qf_eval e (k (lift (rgcdp (eval_poly e p) (eval_poly e q)))).
 Proof.
-move=> Pk p q e; rewrite /rgcdpT !sizeTP; case lqp: (_ < _).  
+move=> Pk p q e; rewrite /rgcdpT !sizeTP; case lqp: (_ < _).
   rewrite isnullP; case q0: (_ == _); first by rewrite Pk (eqP q0) rgcdp0.
-  rewrite sizeTP rgcdp_loopP => [|e' p']; last by rewrite Pk. 
+  rewrite sizeTP rgcdp_loopP => [|e' p']; last by rewrite Pk.
   by rewrite /rgcdp lqp q0.
 rewrite isnullP; case p0: (_ == _); first by rewrite Pk (eqP p0) rgcd0p.
 rewrite sizeTP rgcdp_loopP => [|e' p']; last by rewrite Pk.
@@ -391,7 +391,7 @@ Lemma rgcdpT_qf  (p : polyF) (k : polyF -> formula F) (q : polyF) :
   (forall r, rpoly r -> qf (k r)) -> rpoly p -> rpoly q -> qf (rgcdpT p k q).
 Proof.
 move=> kP rp rq; apply: sizeT_qf=> // n; apply: sizeT_qf=> // m.
-by case:(_ < _); 
+by case: (_ < _);
    apply: isnull_qf=> //; case; do ?apply: kP=> //;
    apply: sizeT_qf=> // n'; apply: rgcdp_loopT_qf.
 Qed.
@@ -467,7 +467,7 @@ Proof. by move=> *; rewrite sizeTP rgdcop_recTP 1?Pk. Qed.
 
 Lemma rgdcopT_qf (p : polyF) (k : polyF -> formula F) (q : polyF) :
   (forall r, rpoly r -> qf (k r)) -> rpoly p -> rpoly q -> qf (rgdcopT p k q).
-Proof. 
+Proof.
 by move=> kP rp rq; apply: sizeT_qf => // n; apply: rgdcop_recT_qf.
 Qed.
 
@@ -505,16 +505,16 @@ Lemma abstrXP  (i : nat) (t : term F) (e : seq F) (x : F) :
   rterm t -> (eval_poly e (abstrX i t)).[x] = eval (set_nth 0 e i x) t.
 Proof.
 elim: t => [n | r | n | t tP s sP | t tP | t tP n | t tP s sP | t tP | t tP n] h.
-- move=> /=; case ni: (_ == _); 
+- move=> /=; case ni: (_ == _);
     rewrite //= ?(mul0r,add0r,addr0,polyC1,mul1r,hornerX,hornerC);
     by rewrite // nth_set_nth /= ni.
 - by rewrite /= mul0r add0r hornerC.
 - by rewrite /= mul0r add0r hornerC.
-- by case/andP: h => *; rewrite /= eval_sumpT hornerD tP ?sP. 
+- by case/andP: h => *; rewrite /= eval_sumpT hornerD tP ?sP.
 - by rewrite /= eval_opppT hornerN tP.
 - by rewrite /= eval_natmulpT hornerMn tP.
 - by case/andP: h => *; rewrite /= eval_mulpT hornerM tP ?sP.
-- by []. 
+- by [].
 - elim: n h => [|n ihn] rt; first by rewrite /= expr0 mul0r add0r hornerC.
   by rewrite /= eval_mulpT exprSr hornerM ihn // mulrC tP.
 Qed.
@@ -576,7 +576,7 @@ Proof.
 move=> e i x; elim=> [|p ps ihps] //=.
 case/andP=> rp rps; rewrite rootE abstrXP //.
 constructor; first by case=> -> hps; rewrite eqxx /=; apply/ihps.
-by case/andP; move/eqP=> -> psr; split=> //; apply/ihps. 
+by case/andP; move/eqP=> -> psr; split=> //; apply/ihps.
 Qed.
 
 Lemma holds_conjn (e : seq F) (i : nat) (x : F) (ps : seq (term F)) :
@@ -587,10 +587,10 @@ Proof.
 elim: ps => [|p ps ihps] //=.
 case/andP=> rp rps; rewrite rootE abstrXP //.
 constructor; first by case=> /eqP-> hps /=; apply/ihps.
-by case/andP=> pr psr; split; first apply/eqP=> //; apply/ihps. 
+by case/andP=> pr psr; split; first apply/eqP=> //; apply/ihps.
 Qed.
 
-Lemma holds_ex_elim : GRing.valid_QE_proj ex_elim.
+Lemma holds_ex_elim: GRing.valid_QE_proj ex_elim.
 Proof.
 move=> i [ps qs] /= e; case/andP=> /= rps rqs.
 rewrite ex_elim_seqP big_map.
@@ -616,7 +616,7 @@ case g0: (\big[(@rgcdp F)/0%:P]_(j <- map (eval_poly e \o abstrX i) ps) j == 0).
   exists x; do 2?constructor=> //; last by apply/holds_conjn.
   apply/holds_conj; rewrite //= -root_biggcd.
   by rewrite (eqp_root (aux _ _ _ )) (eqP g0) root0.
-apply:(iffP (closed_rootP axiom _)); case=> x Px; exists x; move:Px => //=.
+apply: (iffP (closed_rootP axiom _)); case=> x Px; exists x; move: Px => //=.
   rewrite (eqp_root (eqp_rgdco_gdco _ _)) root_gdco ?g0 //.
   rewrite -(eqp_root (aux _ _ _ )) root_biggcd  abstrX_bigmul eval_bigmul.
   rewrite -bigmap_id root_bigmul; case/andP=> psr qsr.
@@ -629,7 +629,7 @@ constructor; first by apply/holds_conj.
 by apply/holds_conjn.
 Qed.
 
-Lemma wf_ex_elim : GRing.wf_QE_proj ex_elim.
+Lemma wf_ex_elim: GRing.wf_QE_proj ex_elim.
 Proof. by move=> i bc /= rbc; apply: ex_elim_qf. Qed.
 
 Definition closed_fields_QEMixin := 
diff --git a/mathcomp/field/countalg.v b/mathcomp/field/countalg.v
index 46ce3a3..95d28cb 100644
--- a/mathcomp/field/countalg.v
+++ b/mathcomp/field/countalg.v
@@ -957,7 +957,7 @@ pose incEp E i j :=
   let v := map_poly (EtoInc E i) (tagged E j) in
   if decode j is [:: i1; k] then
     if i1 == i then odflt v (unpickle k) else v
-  else v. 
+  else v.
 pose fix E_ i := if i is i1.+1 then MkExt _ (incEp (E_ i1) i1) else MkExt F \0.
 pose E i := tag (E_ i); pose Krep := {i : nat & E i}.
 pose fix toEadd i k : {rmorphism E i -> E (k + i)%N} :=
diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v
index 23f5cba..995dbee 100644
--- a/mathcomp/field/falgebra.v
+++ b/mathcomp/field/falgebra.v
@@ -109,7 +109,7 @@ have amE u v : am u v = v * u by rewrite lfunE.
 pose uam := [pred u | lker (am u) == 0%VS].
 pose vam := [fun u => if u \in uam then (am u)^-1%VF 1 else u].
 have vamKl: {in uam, left_inverse 1 vam *%R}.
-  by move=> u Uu; rewrite /= Uu -amE lker0_lfunVK.  
+  by move=> u Uu; rewrite /= Uu -amE lker0_lfunVK.
 exists uam vam => // [u Uu | u v [_ uv1] | u /negbTE/= -> //].
   by apply/(lker0P Uu); rewrite !amE -mulrA vamKl // mul1r mulr1.
 by apply/lker0P=> w1 w2 /(congr1 (am v)); rewrite !amE -!mulrA uv1 !mulr1.
@@ -747,7 +747,7 @@ Qed.
 
 Lemma memvV A u : (u^-1 \in A) = (u \in A).
 Proof.
-suffices{u} invA: invr_closed A by apply/idP/idP=> /invA; rewrite ?invrK. 
+suffices{u} invA: invr_closed A by apply/idP/idP=> /invA; rewrite ?invrK.
 move=> u Au; have [Uu | /invr_out-> //] := boolP (u \is a GRing.unit).
 rewrite memvE -(limg_ker0 _ _ (lker0_amulr Uu)) limg_line lfunE /= mulVr //.
 suff ->: (amulr u @: A)%VS = A by rewrite -memvE -algid_eq1 (unitr_algid1 Au).
@@ -1202,7 +1202,7 @@ Notation "''AHom' ( aT , rT )" := (ahom aT rT) : type_scope.
 Notation "''AEnd' ( aT )" := (ahom aT aT) : type_scope.
 
 Delimit Scope lrfun_scope with AF.
-Bind Scope lrfun_scope with ahom. 
+Bind Scope lrfun_scope with ahom.
 
 Notation "\1" := (@id_ahom _ _) : lrfun_scope.
 Notation "f \o g" := (comp_ahom f g) : lrfun_scope.
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index 234183e..8d2af81 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -870,7 +870,7 @@ Definition vspaceOver V := <<vbasis V : seq L_F>>%VS.
 
 Lemma mem_vspaceOver V : vspaceOver V =i (F * V)%VS.
 Proof.
-move=> y; apply/idP/idP; last rewrite unlock; move=> /coord_span->.
+move=> y; apply/idP/idP; last rewrite unlock; move/coord_span->.
   rewrite (@memv_suml F0 L) // => i _.
   by rewrite memv_mul ?subvsP // vbasis_mem ?memt_nth.
 rewrite memv_suml // => ij _; rewrite -tnth_nth; set x := tnth _ ij.
@@ -1538,7 +1538,7 @@ have nzL1: L1 != 0 by rewrite -(inj_eq toPinj) L1K /toPF raddf0 oner_eq0.
 pose mulM := ComRingMixin mulA mulC mul1 mulD nzL1.
 pose rL := ComRingType (RingType vL mulM) mulC.
 have mulZl: GRing.Lalgebra.axiom mul.
-  move=> a x y; apply: toPinj; rewrite  toL_K /toPF !linearZ /= -!/(toPF _).
+  move=> a x y; apply: toPinj; rewrite toL_K /toPF !linearZ /= -!/(toPF _).
   by rewrite toL_K -scalerAl modp_scalel.
 have mulZr: GRing.Algebra.axiom (LalgType F rL mulZl).
   by move=> a x y; rewrite !(mulrC x) scalerAl.
@@ -1569,6 +1569,8 @@ Qed.
 
 (*Coq 8.3 processes this shorter proof correctly, but then crashes on Qed.
   In Coq 8.4 Qed takes about 18s.
+  In Coq 8.7, everything seems to be all right *)
+(*
 Lemma Xirredp_FAdjoin' (F : fieldType) (p : {poly F}) :
     irreducible_poly p ->
   {L : fieldExtType F & Vector.dim L = (size p).-1 &
@@ -1609,7 +1611,7 @@ have unitE: GRing.Field.mixin_of urL.
   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 apply: leq_gcdpr.
-    rewrite leqNgt;apply:contra;move/eqp_size ->.
+    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.
   congr (poly_rV _); rewrite toL_K modp_mul mulrC (canRL (addKr _) upq1).
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index 17fefe6..eaf5709 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -227,7 +227,7 @@ Qed.
 Lemma kHomExtendP : kHom K <<E; x>> kHomExtend.
 Proof.
 have [fM idKf] := kHomP homKf.
-apply/kHomP; split=> [|z Kz]; last by rewrite kHomExtend_id ?(subvP sKE) ?idKf. 
+apply/kHomP; split=> [|z Kz]; last by rewrite kHomExtend_id ?(subvP sKE) ?idKf.
 move=> _ _ /Fadjoin_polyP[p Ep ->] /Fadjoin_polyP[q Eq ->].
 rewrite -hornerM !kHomExtend_poly ?rpredM // -hornerM; congr _.[_].
 apply/polyP=> i; rewrite coef_map !coefM /= linear_sum /=.
@@ -255,7 +255,7 @@ Proof.
 by move=> sKE eq_fg; rewrite !kAutE (kHom_eq sKE eq_fg) (eq_in_limg eq_fg).
 Qed.
 
-Lemma kAutfE K f : kAut K {:L} f = kHom K {:L} f. 
+Lemma kAutfE K f : kAut K {:L} f = kHom K {:L} f.
 Proof. by rewrite kAutE subvf andbT. Qed.
 
 Lemma kAut1E E (f : 'AEnd(L)) : kAut 1 E f = (f @: E <= E)%VS.
@@ -438,7 +438,7 @@ Lemma normal_field_splitting (F : fieldType) (L : fieldExtType F) :
   SplittingField.axiom L.
 Proof.
 move=> normalL; pose r i := sval (sigW (normalL 1%AS (tnth (vbasis {:L}) i))).
-have sz_r i: size (r i) <= \dim {:L}. 
+have sz_r i: size (r i) <= \dim {:L}.
   rewrite -ltnS -(size_prod_XsubC _ id) /r; case: sigW => _ /= /eqP <-.
   rewrite size_minPoly ltnS; move: (tnth _ _) => x.
   by rewrite adjoin_degreeE dimv1 divn1 dimvS // subvf.
@@ -615,7 +615,7 @@ have [f homLf fxz]: exists2 f : 'End(Lz), kHom 1 imL f & f (inLz x) = z.
     have [q2 Dq2]: exists q2, q1z = map_poly inLz q2.
       exists (\poly_(i < size q1z) (sval (sig_eqW (F0q1z i)))%:A).
       rewrite -{1}[q1z]coefK; apply/polyP=> i; rewrite coef_map !{1}coef_poly.
-      by case: sig_eqW => a; case: ifP; rewrite /= ?rmorph0 ?linearZ ?rmorph1. 
+      by case: sig_eqW => a; case: ifP; rewrite /= ?rmorph0 ?linearZ ?rmorph1.
     rewrite Dq2 dvdp_map minPoly_dvdp //.
       apply/polyOverP=> i; have[a] := F0q1z i.
       rewrite -(rmorph1 [rmorphism of inLz]) -linearZ.
@@ -771,7 +771,7 @@ Variable V : {vspace L}.
 (* The <<_>>, which becomes redundant when V is a {subfield L}, ensures that  *)
 (* the argument of [subg _] is syntactically a group.                         *)
 Inductive gal_of := Gal of [subg kAEnd_group 1 <<V>> / kAEndf (agenv V)].
-Definition gal (f : 'AEnd(L)) := Gal (subg _ (coset _ f)). 
+Definition gal (f : 'AEnd(L)) := Gal (subg _ (coset _ f)).
 Definition gal_sgval x := let: Gal u := x in u.
 
 Fact gal_sgvalK : cancel gal_sgval Gal. Proof. by case. Qed.
@@ -1009,7 +1009,7 @@ Qed.
 Lemma galois_connection K E (A : {set gal_of E}):
   (K <= E)%VS -> (A \subset 'Gal(E / K)) = (K <= fixedField A)%VS.
 Proof.
-move=> sKE; apply/idP/idP => [/fixedFieldS | /(galS E)]. 
+move=> sKE; apply/idP/idP => [/fixedFieldS | /(galS E)].
   by apply: subv_trans; apply galois_connection_subv.
 by apply: subset_trans; apply: galois_connection_subset.
 Qed.
@@ -1143,7 +1143,7 @@ Lemma normalFieldS K M E : (K <= M)%VS -> normalField K E -> normalField M E.
 Proof.
 move=> sKM /normalFieldP nKE; apply/normalFieldP=> a Ea.
 have [r /allP Er splitKa] := nKE a Ea.
-have /dvdp_prod_XsubC[m splitMa]: minPoly M a %| \prod_(b <- r) ('X - b%:P). 
+have /dvdp_prod_XsubC[m splitMa]: minPoly M a %| \prod_(b <- r) ('X - b%:P).
   by rewrite -splitKa minPolyS.
 exists (mask m r); first by apply/allP=> b /mem_mask/Er.
 by apply/eqP; rewrite -eqp_monic ?monic_prod_XsubC ?monic_minPoly.
@@ -1169,7 +1169,7 @@ have sXE := basis_mem (vbasisP E); set X : seq L := vbasis E in sXE.
 exists (\prod_(a <- X) minPoly K a).
   by apply: rpred_prod => a _; apply: minPolyOver.
 exists (flatten [seq (sval (rK_ a)) | a <- X]).
-  move/allP: sXE; elim: X => [|a X IHX] ; first by rewrite !big_nil eqpxx.
+  move/allP: sXE; elim: X => [|a X IHX]; first by rewrite !big_nil eqpxx.
   rewrite big_cons /= big_cat /= => /andP[Ea sXE].
   by case: (rK_ a) => /= r [] // _ <-; apply/eqp_mull/IHX.
 apply/eqP; rewrite eqEsubv; apply/andP; split.
@@ -1215,7 +1215,7 @@ Lemma normalField_factors K E :
    (normalField K E).
 Proof.
 move=> sKE; apply: (iffP idP) => [nKE a Ea | nKE]; last first.
-  apply/normalFieldP=> a Ea; have [r _ ->] := nKE a Ea. 
+  apply/normalFieldP=> a Ea; have [r _ ->] := nKE a Ea.
   exists [seq x a | x : gal_of E <- r]; last by rewrite big_map.
   by rewrite all_map; apply/allP=> b _; apply: memv_gal.
 have [r Er splitKa] := normalFieldP nKE a Ea.
@@ -1312,7 +1312,7 @@ apply (iffP idP) => [/and3P[sKE /separableP sepKE nKE] | fixedKE].
   rewrite -eqSS -size_minPoly splitKa size_prod_XsubC eqSS -/(size [:: a]).
   have Ur: uniq r by rewrite -separable_prod_XsubC -splitKa; apply: sepKE.
   rewrite -uniq_size_uniq {Ur}// => b; rewrite inE -root_prod_XsubC -splitKa.
-  apply/eqP/idP=> [-> | pKa_b_0]; first exact: root_minPoly. 
+  apply/eqP/idP=> [-> | pKa_b_0]; first exact: root_minPoly.
   by have [x /fixEa-> ->] := normalField_root_minPoly sKE nKE Ea pKa_b_0.
 have sKE: (K <= E)%VS by rewrite -fixedKE capvSl.
 apply/galois_factors=> // a Ea.
@@ -1321,7 +1321,7 @@ have /fin_all_exists2[x_ galEx_ Dx_a] (b : seq_sub r_pKa) := imageP (valP b).
 exists (codom x_); rewrite -map_comp; set r := map _ _.
 have r_xa x: x \in 'Gal(E / K) -> x a \in r.
   move=> galEx; have r_pKa_xa: x a \in r_pKa by apply/imageP; exists x.
-  by rewrite [x a](Dx_a (SeqSub r_pKa_xa)); apply: codom_f. 
+  by rewrite [x a](Dx_a (SeqSub r_pKa_xa)); apply: codom_f.
 have Ur: uniq r by apply/injectiveP=> b c /=; rewrite -!Dx_a => /val_inj.
 split=> //; first by apply/subsetP=> _ /codomP[b ->].
 apply/eqP; rewrite -eqp_monic ?monic_minPoly ?monic_prod_XsubC //.
@@ -1389,10 +1389,10 @@ have [x1 | ntx] := eqVneq x 1%g.
   by rewrite -{1}normEa1 /galNorm DgalE x1 cycle1 big_set1 !gal_id divr1.
 pose c_ y := \prod_(i < invm (injm_Zpm x) y) (x ^+ i)%g a.
 have nz_c1: c_ 1%g != 0 by rewrite /c_ morph1 big_ord0 oner_neq0.
-have [d] := @gal_independent_contra _ (mem 'Gal(E / K)) _ _ (group1 _) nz_c1. 
+have [d] := @gal_independent_contra _ (mem 'Gal(E / K)) _ _ (group1 _) nz_c1.
 set b := \sum_(y in _) _ => Ed nz_b; exists b.
   split=> //; apply: rpred_sum => y galEy.
-  by apply: rpredM; first apply:  rpred_prod => i _; apply: memv_gal.
+  by apply: rpredM; first apply: rpred_prod => i _; apply: memv_gal.
 apply: canRL (mulfK _) _; first by rewrite fmorph_eq0.
 rewrite rmorph_sum mulr_sumr [b](reindex_acts 'R _ galEx) ?astabsR //=.
 apply: eq_bigr => y galEy; rewrite galM // rmorphM mulrA; congr (_ * _).
@@ -1477,7 +1477,7 @@ rewrite mulrC memv_mul ?memv_line //; apply/fixedFieldP=> [|x Gx].
   have Edet n (N : 'M_n) (E_N : forall i j, N i j \in E): \det N \in E.
     by apply: rpred_sum => sigma _; rewrite rpredMsign rpred_prod.
   rewrite /invmx uM 2!mxE mulrC rpred_div ?Edet //.
-  by rewrite rpredMsign Edet // => k l; rewrite 2!mxE.  
+  by rewrite rpredMsign Edet // => k l; rewrite 2!mxE.
 suffices{i} {2}<-: map_mx x v = v by rewrite [map_mx x v i 0]mxE.
 have uMx: map_mx x (M w) \in unitmx by rewrite map_unitmx.
 rewrite map_mxM map_invmx /=; apply: canLR {uMx}(mulKmx uMx) _.
diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v
index 6178c01..c3f3ebb 100644
--- a/mathcomp/field/separable.v
+++ b/mathcomp/field/separable.v
@@ -71,13 +71,13 @@ apply: (iffP idP) => [sep_p | [sq'p nz_der1p]].
   split=> [u v | u u_dv_p]; last first.
     apply: contraTneq => u'0; rewrite -leqNgt -(eqnP sep_p).
     rewrite dvdp_leq -?size_poly_eq0 ?(eqnP sep_p) // dvdp_gcd u_dv_p.
-    have /dvdp_scaler <-: lead_coef u ^+ scalp p u != 0 by rewrite lcn_neq0. 
+    have /dvdp_scaler <-: lead_coef u ^+ scalp p u != 0 by rewrite lcn_neq0.
     by rewrite -derivZ -Pdiv.Idomain.divpK //= derivM u'0 mulr0 addr0 dvdp_mull.
   rewrite Pdiv.Idomain.dvdp_eq mulrCA mulrA; set c := _ ^+ _ => /eqP Dcp.
   have nz_c: c != 0 by rewrite lcn_neq0.
   move: sep_p; rewrite coprimep_sym -[separable _](coprimep_scalel _ _ nz_c).
   rewrite -(coprimep_scaler _ _ nz_c) -derivZ Dcp derivM coprimep_mull.
-  by rewrite coprimep_addl_mul !coprimep_mulr -andbA => /and4P[]. 
+  by rewrite coprimep_addl_mul !coprimep_mulr -andbA => /and4P[].
 rewrite /separable coprimep_def eqn_leq size_poly_gt0; set g := gcdp _ _.
 have nz_g: g != 0.
   rewrite -dvd0p dvdp_gcd -(mulr0 0); apply/nandP; left.
@@ -217,7 +217,7 @@ pose kappa' := inj_subfx iota z r1.
 have /eq_map_poly Diota: kappa \o kappa' =1 iota.
   by move=> w; rewrite /kappa /= subfx_inj_eval // map_polyC hornerC.
 suffices [y3]: exists y3, y = kappa y3.
-  have [q3 ->] := subfxE y3; rewrite /kappa subfx_inj_eval // => Dy.  
+  have [q3 ->] := subfxE y3; rewrite /kappa subfx_inj_eval // => Dy.
   split; [exists (t *: q3 - 'X) | by exists q3].
   by rewrite rmorphB linearZ /= map_polyX !hornerE -Dy opprB addrC addrNK.
 pose p0 := p ^ iota \Po (iota t *: 'X - z%:P).
@@ -244,7 +244,7 @@ have{p0} [p3 ->]: exists p3, p0 = p3 ^ kappa.
 rewrite -Diota map_poly_comp -gcdp_map /= -/kappa.
 move: (gcdp _ _) => r3 /eqpf_eq[c nz_c Dr3].
 exists (- (r3`_0 / r3`_1)); rewrite [kappa _]rmorphN fmorph_div -!coef_map Dr3.
-by rewrite !coefZ polyseqXsubC mulr1 mulrC mulKf ?opprK. 
+by rewrite !coefZ polyseqXsubC mulr1 mulrC mulKf ?opprK.
 Qed.
 
 Lemma char0_PET (q : {poly F}) :
@@ -534,7 +534,7 @@ have Dder: Derivation <<K; x>> D.
   apply/allP=> u /vbasis_mem Kx_u; apply/allP=> v /vbasis_mem Kx_v.
   rewrite !lfunE /= -{-2}(Fadjoin_poly_eq Kx_u) -{-3}(Fadjoin_poly_eq Kx_v).
   rewrite -!hornerM -hornerD -derivM.
-  rewrite Fadjoin_poly_mod ?rpredM ?Fadjoin_polyOver //. 
+  rewrite Fadjoin_poly_mod ?rpredM ?Fadjoin_polyOver //.
   rewrite {2}(divp_eq (_ * _) (minPoly K x)) derivD derivM pKx'_0 mulr0 addr0.
   by rewrite hornerD hornerM minPolyxx mulr0 add0r.
 have{Dder DK_0}: x \in lker D by apply: subvP Kx_x; apply: derKx_0.
@@ -608,7 +608,7 @@ Lemma charf_p_separable K x e p :
   p \in [char L] -> separable_element K x = (x \in <<K; x ^+ (p ^ e.+1)>>%VS).
 Proof.
 move=> charLp; apply/idP/idP=> [sepKx | /Fadjoin_poly_eq]; last first.
-  set m := p ^ _;set f := Fadjoin_poly K _ x => Dx; apply/separable_elementP.
+  set m := p ^ _; set f := Fadjoin_poly K _ x => Dx; apply/separable_elementP.
   have mL0: m%:R = 0 :> L by apply/eqP; rewrite -(dvdn_charf charLp) dvdn_exp.
   exists ('X - (f \Po 'X^m)); split.
   - by rewrite rpredB ?polyOver_comp ?rpredX ?polyOverX ?Fadjoin_polyOver.
@@ -672,7 +672,7 @@ Lemma separable_inseparable_element K x :
 Proof.
 rewrite /purely_inseparable_element; case: ex_minnP => [[|m]] //=.
 rewrite subfield_closed; case: m => /= [-> //| m _ /(_ 1%N)/implyP/= insepKx].
-by rewrite (negPf insepKx) (contraNF (@base_separable K x) insepKx). 
+by rewrite (negPf insepKx) (contraNF (@base_separable K x) insepKx).
 Qed.
 
 Lemma base_inseparable K x : x \in K -> purely_inseparable_element K x.