running semi-automated linting on the whole library

12 files changed, 114 insertions, 113 deletions

diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v
index 0cf29b2..3a50934 100644
--- a/mathcomp/algebra/finalg.v
+++ b/mathcomp/algebra/finalg.v
@@ -883,7 +883,7 @@ Section ClassDef.
 Variable R : ringType.
 
 Record class_of M :=
-  Class { base : GRing.Lmodule.class_of R M ; mixin : mixin_of M base }.
+  Class { base : GRing.Lmodule.class_of R M; mixin : mixin_of M base }.
 Definition base2 R (c : class_of R) := Zmodule.Class (mixin c).
 Local Coercion base : class_of >-> GRing.Lmodule.class_of.
 Local Coercion base2 : class_of >-> Zmodule.class_of.
@@ -1144,7 +1144,7 @@ Section ClassDef.
 Variable R : unitRingType.
  
 Record class_of M := 
-  Class { base : GRing.UnitAlgebra.class_of R M ; mixin : mixin_of M base }. 
+  Class { base : GRing.UnitAlgebra.class_of R M; mixin : mixin_of M base }.
 Definition base2 M (c : class_of M) := Algebra.Class (mixin c).
 Definition base3 M (c : class_of M) := @UnitRing.Class _ (base c) (mixin c).
 
@@ -1155,27 +1155,27 @@ Local Coercion base3 : class_of >-> UnitRing.class_of.
 Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
 Local Coercion sort : type >-> Sortclass.
 Variables (phR : phant R) (cT : type phR).
-Definition pack := gen_pack (Pack phR) Class (@GRing.UnitAlgebra.class R phR). 
+Definition pack := gen_pack (Pack phR) Class (@GRing.UnitAlgebra.class R phR).
 Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
 Let xT := let: Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT. 
-Definition choiceType := @Choice.Pack cT xclass xT. 
-Definition countType := @Countable.Pack cT (fin_ xclass) xT. 
-Definition finType := @Finite.Pack cT (fin_ xclass) xT. 
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. 
-Definition finZmodType := @Zmodule.Pack cT xclass xT. 
-Definition ringType := @GRing.Ring.Pack cT xclass xT. 
-Definition finRingType := @Ring.Pack cT xclass xT. 
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (fin_ xclass) xT.
+Definition finType := @Finite.Pack cT (fin_ xclass) xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition finZmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition finRingType := @Ring.Pack cT xclass xT.
 Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition finUnitRingType := @UnitRing.Pack cT xclass xT. 
-Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT. 
-Definition finLmodType := @Lmodule.Pack R phR cT xclass xT. 
-Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT. 
-Definition finLalgType := @Lalgebra.Pack R phR cT xclass xT. 
-Definition algType := @GRing.Algebra.Pack R phR cT xclass xT. 
-Definition finAlgType := @Algebra.Pack R phR cT xclass xT. 
+Definition finUnitRingType := @UnitRing.Pack cT xclass xT.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
+Definition finLmodType := @Lmodule.Pack R phR cT xclass xT.
+Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.
+Definition finLalgType := @Lalgebra.Pack R phR cT xclass xT.
+Definition algType := @GRing.Algebra.Pack R phR cT xclass xT.
+Definition finAlgType := @Algebra.Pack R phR cT xclass xT.
 Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass xT.
 
 Definition join_finType := @Finite.Pack unitAlgType (fin_ xclass) xT.
@@ -1200,7 +1200,7 @@ Definition finGroupType := fin_group baseFinGroupType zmodType.
 Definition join_baseFinGroupType := base_group unitAlgType zmodType finType.
 Definition join_finGroupType := fin_group join_baseFinGroupType zmodType.
 
-End ClassDef. 
+End ClassDef.
 
 Module Exports.
 Coercion base : class_of >-> GRing.UnitAlgebra.class_of.
@@ -1290,7 +1290,7 @@ End FinRing.
 Import FinRing.
 Export Zmodule.Exports Ring.Exports ComRing.Exports.
 Export UnitRing.Exports UnitsGroupExports ComUnitRing.Exports.
-Export IntegralDomain.Exports Field.Exports DecField.Exports.    
+Export IntegralDomain.Exports Field.Exports DecField.Exports.
 Export Lmodule.Exports Lalgebra.Exports Algebra.Exports UnitAlgebra.Exports.
 
 Notation "{ 'unit' R }" := (unit_of (Phant R))
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 7c99443..a85b3ec 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -223,7 +223,7 @@ Proof. by move=> d_gt0; rewrite !lerNgt ltz_divLR. Qed.
 Lemma divz_ge0 m d : d > 0 -> ((m %/ d)%Z >= 0) = (m >= 0).
 Proof. by case: d m => // d [] n d_gt0; rewrite (divz_nat, divNz_nat). Qed.
 
-Lemma divzMA_ge0 m n p : n >= 0 -> (m %/ (n * p) = (m %/ n)%Z %/ p)%Z. 
+Lemma divzMA_ge0 m n p : n >= 0 -> (m %/ (n * p) = (m %/ n)%Z %/ p)%Z.
 Proof.
 case: n => // [[|n]] _; first by rewrite mul0r !divz0 div0z.
 wlog p_gt0: p / p > 0; last case: p => // p in p_gt0 *.
@@ -457,7 +457,7 @@ Lemma Qint_dvdz (m d : int) : (d %| m)%Z -> ((m%:~R / d%:~R : rat) \is a Qint).
 Proof.
 case/dvdzP=> z ->; rewrite rmorphM /=; case: (altP (d =P 0)) => [->|dn0].
   by rewrite mulr0 mul0r.
-by rewrite mulfK ?intr_eq0 // rpred_int. 
+by rewrite mulfK ?intr_eq0 // rpred_int.
 Qed.
 
 Lemma Qnat_dvd (m d : nat) : (d %| m)%N -> ((m%:R / d%:R : rat) \is a Qnat).
@@ -934,7 +934,7 @@ wlog [j a'Mij]: m n M i Da le_mn / {j | ~~ (a %| M i j)%Z}; last first.
   have uU: U \in unitmx.
     rewrite unitmxE det_ublock det1 (expand_det_col _ 0) big_ord_recl big_ord1.
     do 2!rewrite /cofactor [row' _ _]mx11_scalar !mxE det_scalar1 /=.
-    rewrite mulr1 mul1r mulN1r opprK -[_ + _](mulzK _ nz_b) mulrDl. 
+    rewrite mulr1 mul1r mulN1r opprK -[_ + _](mulzK _ nz_b) mulrDl.
     by rewrite -!mulrA !divzK ?dvdz_gcdl ?dvdz_gcdr // Db divzz nz_b unitr1.
   have{Db} Db: M1 i 0 = b.
     rewrite /M1 -(lshift0 n 1) [U]block_mxEh mul_mx_row row_mxEl.
@@ -952,9 +952,9 @@ move=> {A leA IHa} IHa; wlog Di: i M Da / i = 0; last rewrite {i}Di in Da.
   by rewrite mulmxA -perm_mxM tperm2 perm_mx1 mul1mx.
 without loss /forallP a_dvM0: / [forall j, a %| M 0 j]%Z.
   have [_|] := altP forallP; first exact; rewrite negb_forall => /existsP/sigW.
-  by move/IHa=> IH _; apply: IH. 
+  by move/IHa=> IH _; apply: IH.
 without loss{Da a_dvM0} Da: M / forall j, M 0 j = a.
-  pose Uur := col' 0 (\row_j (1 - (M 0 j %/ a)%Z)). 
+  pose Uur := col' 0 (\row_j (1 - (M 0 j %/ a)%Z)).
   pose U : 'M_(1 + n) := block_mx 1 Uur 0 1%:M; pose M1 := M *m U.
   have uU: U \in unitmx by rewrite unitmxE det_ublock !det1 mulr1.
   case/(_ (M *m U)) => [j | L uL [R uR [d dvD dM]]].
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 56dec94..e269752 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -230,7 +230,7 @@ Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
 
 Lemma itvP : forall (x : R) (i : interval R), (x \in i) -> itv_rewrite i x.
 Proof.
-move=> x [[[] a|] [[] b|]]; move/itv_dec=> //= [hl hu];do ?[split=> //;
+move=> x [[[] a|] [[] b|]]; move/itv_dec=> //= [hl hu]; do ?[split=> //;
   do ?[by rewrite ltrW | by rewrite ltrWN | by rewrite ltrNW |
     by rewrite (ltr_geF, ler_gtF)]];
   rewrite ?(bound_in_itv) /le_boundl /le_boundr //=; do ?
@@ -254,7 +254,7 @@ Lemma subitvP : forall (i2 i1 : interval R),
   (subitv i1 i2) -> {subset i1 <= i2}.
 Proof.
 by move=> [[[] a2|] [[] b2|]] [[[] a1|] [[] b1|]];
-  rewrite /subitv //; case/andP=> /= ha hb; move=> x hx; rewrite ?inE;
+  rewrite /subitv //; case/andP=> /= ha hb x hx; rewrite ?inE;
     rewrite ?(ler_trans ha) ?(ler_lt_trans ha) ?(ltr_le_trans ha) //;
       rewrite ?(ler_trans _ hb) ?(ltr_le_trans _ hb) ?(ler_lt_trans _ hb) //;
         rewrite ?(itvP hx) //.
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index dfa8474..aecbce9 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -864,7 +864,7 @@ Section VecMatrix.
 
 Variables m n : nat.
 
-Lemma mxvec_cast : #|{:'I_m * 'I_n}| = (m * n)%N. 
+Lemma mxvec_cast : #|{:'I_m * 'I_n}| = (m * n)%N.
 Proof. by rewrite card_prod !card_ord. Qed.
 
 Definition mxvec_index (i : 'I_m) (j : 'I_n) :=
@@ -973,7 +973,7 @@ Proof. by apply/matrixP=> i j; rewrite !(castmxE, mxE). Qed.
 Lemma map_conform_mx m' n' (B : 'M_(m', n')) :
   (conform_mx B A)^f = conform_mx B^f A^f.
 Proof.
-move: B; have [[<- <-] B|] := eqVneq (m, n) (m', n'). 
+move: B; have [[<- <-] B|] := eqVneq (m, n) (m', n').
   by rewrite !conform_mx_id.
 by rewrite negb_and => neq_mn B; rewrite !nonconform_mx.
 Qed.
@@ -1197,7 +1197,7 @@ Lemma nz_row_eq0 m n (A : 'M_(m, n)) : (nz_row A == 0) = (A == 0).
 Proof.
 rewrite /nz_row; symmetry; case: pickP => [i /= nzAi | Ai0].
   by rewrite (negbTE nzAi); apply: contraTF nzAi => /eqP->; rewrite row0 eqxx.
-by rewrite eqxx; apply/eqP/row_matrixP=> i; move/eqP: (Ai0 i) ->; rewrite row0. 
+by rewrite eqxx; apply/eqP/row_matrixP=> i; move/eqP: (Ai0 i) ->; rewrite row0.
 Qed.
 
 End MatrixZmodule.
@@ -1755,7 +1755,7 @@ Lemma mul_pid_mx m n p q r :
   (pid_mx q : 'M_(m, n)) *m (pid_mx r : 'M_(n, p)) = pid_mx (minn n (minn q r)).
 Proof.
 apply/matrixP=> i k; rewrite !mxE !leq_min.
-have [le_n_i | lt_i_n] := leqP n i. 
+have [le_n_i | lt_i_n] := leqP n i.
   rewrite andbF big1 // => j _.
   by rewrite -pid_mx_minh !mxE leq_min ltnNge le_n_i andbF mul0r.
 rewrite (bigD1 (Ordinal lt_i_n)) //= big1 ?addr0 => [|j].
@@ -1903,7 +1903,7 @@ move=> a A B; apply/row_matrixP; case/mxvec_indexP=> i j.
 rewrite linearP /= !rowE !mul_rV_lin /= vec_mx_delta -linearP mulmxDr.
 congr (mxvec (_ + _)); apply/row_matrixP=> k.
 rewrite linearZ /= !row_mul rowE mul_delta_mx_cond.
-by case: (k == i); [rewrite -!rowE linearZ | rewrite !mul0mx raddf0]. 
+by case: (k == i); [rewrite -!rowE linearZ | rewrite !mul0mx raddf0].
 Qed.
 Canonical lin_mulmxr_additive := Additive lin_mulmxr_is_linear.
 Canonical lin_mulmxr_linear := Linear lin_mulmxr_is_linear.
@@ -2810,7 +2810,7 @@ Proof. exact: map_unitmx. Qed.
 Lemma map_invmx n (A : 'M_n) : (invmx A)^f = invmx A^f.
 Proof.
 rewrite /invmx map_unitmx (fun_if ((map_mx f) n n)).
-by rewrite map_mxZ map_mx_adj det_map_mx fmorphV. 
+by rewrite map_mxZ map_mx_adj det_map_mx fmorphV.
 Qed.
 
 Lemma map_mx_inv n' (A : 'M_n'.+1) : A^-1^f = A^f^-1.
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 1b6200e..463f07b 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -658,7 +658,7 @@ Qed.
 Lemma submx_full m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
   row_full B -> (A <= B)%MS.
 Proof.
-by rewrite submxE /cokermx =>/eqnP->; rewrite /copid_mx pid_mx_1 subrr !mulmx0.
+by rewrite submxE /cokermx => /eqnP->; rewrite /copid_mx pid_mx_1 subrr !mulmx0.
 Qed.
 
 Lemma row_fullP m n (A : 'M_(m, n)) :
@@ -700,7 +700,7 @@ Lemma row_full_unit n (A : 'M_n) : row_full A = (A \in unitmx).
 Proof. exact: row_free_unit. Qed.
   
 Lemma mxrank_unit n (A : 'M_n) : A \in unitmx -> \rank A = n.
-Proof. by rewrite -row_full_unit =>/eqnP. Qed.
+Proof. by rewrite -row_full_unit => /eqnP. Qed.
 
 Lemma mxrank1 n : \rank (1%:M : 'M_n) = n.
 Proof. by apply: mxrank_unit; apply: unitmx1. Qed.
@@ -1114,7 +1114,7 @@ Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) :
           (A <= \sum_(i | P i) B_ i)%MS.
 Proof.
 apply: (iffP idP) => [| [u_ ->]]; last first.
-  by apply: summx_sub_sums => i _; apply: submxMl. 
+  by apply: summx_sub_sums => i _; apply: submxMl.
 elim: {P}_.+1 {-2}P A (ltnSn #|P|) => // b IHb P A.
 case: (pickP P) => [i Pi | P0 _]; last first.
   rewrite big_pred0 //; move/submx0null->.
@@ -1202,7 +1202,7 @@ Lemma mxrank_Frobenius m n p q (A : 'M_(m, n)) B (C : 'M_(p, q)) :
 Proof.
 rewrite -{2}(mulmx_base (A *m B)) -mulmxA (eqmxMfull _ (col_base_full _)).
 set C2 := row_base _ *m C.
-rewrite -{1}(subnK (rank_leq_row C2)) -(mxrank_ker C2) addnAC leq_add2r. 
+rewrite -{1}(subnK (rank_leq_row C2)) -(mxrank_ker C2) addnAC leq_add2r.
 rewrite addnC -{1}(mulmx_base B) -mulmxA eqmxMfull //.
 set C1 := _ *m C; rewrite -{2}(subnKC (rank_leq_row C1)) leq_add2l -mxrank_ker.
 rewrite -(mxrankMfree _ (row_base_free (A *m B))).
@@ -1466,7 +1466,7 @@ apply/eqP; set K := kermx B; set C := (A :&: K)%MS.
 rewrite -(eqmxMr B (eq_row_base A)); set K' := _ *m B.
 rewrite -{2}(subnKC (rank_leq_row K')) -mxrank_ker eqn_add2l.
 rewrite -(mxrankMfree _ (row_base_free A)) mxrank_leqif_sup.
-  rewrite sub_capmx -(eq_row_base A) submxMl. 
+  rewrite sub_capmx -(eq_row_base A) submxMl.
   by apply/sub_kermxP; rewrite -mulmxA mulmx_ker.
 have /submxP[C' defC]: (C <= row_base A)%MS by rewrite eq_row_base capmxSl.
 rewrite defC submxMr //; apply/sub_kermxP.
@@ -1573,7 +1573,7 @@ Proof.
 move=> dxUV sWU; apply/eqP; rewrite -subr_eq0 -submx0 -dxUV.
 rewrite sub_capmx addmx_sub ?eqmx_opp ?proj_mx_sub //= -eqmx_opp opprB.
 by rewrite proj_mx_compl_sub // (submx_trans sWU) ?addsmxSl.
-Qed. 
+Qed.
 
 Lemma proj_mx_0 m n U V (W : 'M_(m, n)) :
   (U :&: V = 0)%MS -> (W <= V)%MS -> W *m proj_mx U V = 0.
@@ -1845,7 +1845,7 @@ Proof.
 rewrite /TIsum; apply: (iffP eqnP) => /= [dxS i Pi | dxS].
   set Si' := (\sum_(j | _) unwrap (S_ j))%MS.
   have: mxdirect (unwrap (S_ i) + Si') by apply/eqnP; rewrite /= -!(bigD1 i).
-  by rewrite mxdirect_addsE => /and3P[-> _ /eqP].  
+  by rewrite mxdirect_addsE => /and3P[-> _ /eqP].
 elim: _.+1 {-2 4}P (subxx P) (ltnSn #|P|) => // m IHm Q; move/subsetP=> sQP.
 case: (pickP Q) => [i Qi | Q0]; last by rewrite !big_pred0 ?mxrank0.
 rewrite (cardD1x Qi) !((bigD1 i) Q) //=.
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index eeece16..4d043ea 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -147,7 +147,7 @@ Proof.
 move=> p_nc q_nc; pose dp := (size p).-1; pose dq := (size q).-1.
 pose S := Sylvester_mx p q; pose dS := (dq + dp)%N.
 have dS_gt0: dS > 0 by rewrite /dS /dq -(subnKC q_nc).
-pose j0 := Ordinal dS_gt0. 
+pose j0 := Ordinal dS_gt0.
 pose Ss0 := col_mx (p *: \col_(i < dq) 'X^i) (q *: \col_(i < dp) 'X^i).
 pose Ss := \matrix_(i, j) (if j == j0 then Ss0 i 0 else (S i j)%:P).
 pose u ds s := \sum_(i < ds) cofactor Ss (s i) j0 * 'X^i.
@@ -325,13 +325,13 @@ apply: leq_trans (_ : #|[pred j | s j == j]|.+1 <= n.-1).
   - by rewrite size_poly1.
   - apply: leq_trans (size_mul_leq _ _) _.
     by rewrite -subn1 -addnS leq_subLR addnA leq_add.
-  rewrite !mxE eq_sym !inE; case: (s j == j); first by rewrite polyseqXsubC. 
+  rewrite !mxE eq_sym !inE; case: (s j == j); first by rewrite polyseqXsubC.
   by rewrite sub0r size_opp size_polyC leq_b1.
 rewrite -{8}[n]card_ord -(cardC (pred2 (s i) i)) card2 nfix_i !ltnS.
 apply: subset_leq_card; apply/subsetP=> j; move/(_ =P j)=> fix_j.
 rewrite !inE -{1}fix_j (inj_eq (@perm_inj _ s)) orbb.
 by apply: contraNneq nfix_i => <-; rewrite fix_j.
-Qed.   
+Qed.
 
 Lemma size_char_poly : size char_poly = n.+1.
 Proof.
@@ -356,7 +356,7 @@ have ->: \tr A = \sum_(x <- diagA) x by rewrite big_map enumT.
 rewrite -size_diagA {}/p; elim: diagA => [|x d IHd].
   by rewrite !big_nil mulr1 coefX oppr0.
 rewrite !big_cons coefXM mulrBl coefB IHd opprD addrC; congr (- _ + _).
-rewrite mul_polyC coefZ [size _]/= -(size_prod_XsubC _ id) -lead_coefE. 
+rewrite mul_polyC coefZ [size _]/= -(size_prod_XsubC _ id) -lead_coefE.
 by rewrite (monicP _) ?monic_prod_XsubC ?mulr1.
 Qed.
 
@@ -591,7 +591,7 @@ Variables (d n : nat) (A : 'M[aR]_n).
 Lemma map_rVpoly (u : 'rV_d) : fp (rVpoly u) = rVpoly u^f.
 Proof.
 apply/polyP=> k; rewrite coef_map !coef_rVpoly.
-by case: (insub k) => [i|]; rewrite  /=  ?rmorph0 // mxE.
+by case: (insub k) => [i|]; rewrite /=  ?rmorph0 // mxE.
 Qed.
 
 Lemma map_poly_rV p : (poly_rV p)^f = poly_rV (fp p) :> 'rV_d.
@@ -817,7 +817,7 @@ rewrite polySpred ?monic_neq0 // -/m1 big_ord_recr /= -lead_coefE.
 rewrite opprD addrC (monicP mon_p) mul1r subrK !mulrN -mulNr !mulr_sumr.
 apply: Msum => j _; rewrite mulrA mulrACA -exprD; apply: IHn.
   by rewrite -addnS addnC addnBA // leq_subLR leq_add.
-by rewrite -mulN1r; do 2!apply: (genM) => //; apply: genR. 
+by rewrite -mulN1r; do 2!apply: (genM) => //; apply: genR.
 Qed.
 
 Lemma integral_root_monic u p :
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 56493dd..5e684a1 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -564,7 +564,7 @@ pose dp := (size p).-1; pose dq := (size q).-1.
 have [-> | nz_p] := eqVneq p 0; first by rewrite lead_coef0 !mul0r coef0.
 have [-> | nz_q] := eqVneq q 0; first by rewrite lead_coef0 !mulr0 coef0.
 have ->: (size p + size q).-2 = (dp + dq)%N.
-  by do 2! rewrite polySpred // addSn addnC.
+  by do 2!rewrite polySpred // addSn addnC.
 have lt_p_pq: dp < (dp + dq).+1 by rewrite ltnS leq_addr.
 rewrite coefM (bigD1 (Ordinal lt_p_pq)) ?big1 ?simp ?addKn //= => i.
 rewrite -val_eqE neq_ltn /= => /orP[lt_i_p | gt_i_p]; last first.
@@ -1271,7 +1271,7 @@ End OnePrimitive.
 Lemma prim_root_exp_coprime n z k :
   n.-primitive_root z -> n.-primitive_root (z ^+ k) = coprime k n.
 Proof.
-move=> prim_z;have n_gt0 := prim_order_gt0 prim_z.
+move=> prim_z; have n_gt0 := prim_order_gt0 prim_z.
 apply/idP/idP=> [prim_zk | co_k_n].
   set d := gcdn k n; have dv_d_n: (d %| n)%N := dvdn_gcdr _ _.
   rewrite /coprime -/d -(eqn_pmul2r n_gt0) mul1n -{2}(gcdnMl n d).
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index b5e1068..b6f8936 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -235,7 +235,7 @@ have -> /= : (size r).-1 < size q + j.
   by rewrite -{1}[_.-1]add0n ltn_add2r.
 move: (hj); rewrite leq_eqVlt; case/orP.
   move/eqP<-; rewrite -{1}(prednK sq) -{3}(prednK sr) subSS.
-  rewrite  subKn; first by rewrite coefMC !lead_coefE subrr.
+  rewrite subKn; first by rewrite coefMC !lead_coefE subrr.
   by move: hsrq; rewrite -{1}(prednK sq) -{1}(prednK sr) ltnS.
 move=> {hj} hj; move: (hj); rewrite prednK // coefMC; move/leq_sizeP=> -> //.
 suff: size q <= j - (size r - size q).
@@ -573,7 +573,7 @@ Lemma redivp_eq q r :  size r < size d ->
   redivp (q * d + r) d = (k, q, r).
 Proof.
 case: (monic_comreg mond)=> Hc Hr; move/(redivp_eq Hc Hr q).
-by rewrite  (eqP mond); move=> -> /=; rewrite expr1n !mulr1.
+by rewrite (eqP mond) => -> /=; rewrite expr1n !mulr1.
 Qed.
 
 Lemma rdivp_eq p :
@@ -670,7 +670,7 @@ Qed.
 Lemma rdvdpP p : reflect (exists qq, p = qq * d) (rdvdp d p).
 Proof.
 case: (monic_comreg mond)=> Hc Hr; apply: (iffP idP).
-  case: rdvdp_eqP=> // k qq; rewrite (eqP mond) expr1n mulr1; move=> -> _.
+  case: rdvdp_eqP=> // k qq; rewrite (eqP mond) expr1n mulr1 => -> _.
   by exists qq.
 by case=> [qq]; move/eq_rdvdp.
 Qed.
@@ -892,7 +892,7 @@ rewrite unlock ud redivp_def; constructor => //.
   have hn0 : (lead_coef d ^+ rscalp m d)%:P != 0.
     by rewrite polyC_eq0; apply: expf_neq0.
   apply: (mulfI hn0); rewrite !mulrA -exprVn !polyC_exp -exprMn -polyC_mul.
-  by rewrite  divrr // expr1n mul1r -polyC_exp mul_polyC rdivp_eq.
+  by rewrite divrr // expr1n mul1r -polyC_exp mul_polyC rdivp_eq.
 move=> dn0; rewrite size_scale ?ltn_rmodp // -exprVn expf_eq0 negb_and.
 by rewrite invr_eq0 cdn0 orbT.
 Qed.
@@ -905,7 +905,7 @@ move=> hsrd hu; rewrite unlock hu; case et: (redivp _ _) => [[s qq] rr].
 have cdn0 : lead_coef d != 0.
   by move: hu; case d0: (lead_coef d == 0) => //; rewrite (eqP d0) unitr0.
 move: (et); rewrite RingComRreg.redivp_eq //; last by apply/rregP.
-rewrite et /=; case => e1 e2; rewrite -!mul_polyC -!exprVn !polyC_exp.
+rewrite et /=; case=> e1 e2; rewrite -!mul_polyC -!exprVn !polyC_exp.
 suff h x y: x * (lead_coef d ^+ s)%:P = y -> ((lead_coef d)^-1)%:P ^+ s * y = x.
   by congr (_, _, _); apply: h.
 have hn0 : (lead_coef d)%:P ^+ s != 0 by apply: expf_neq0; rewrite polyC_eq0.
@@ -1030,7 +1030,7 @@ Qed.
 
 Lemma divp1 m : m %/ 1 = m.
 Proof.
-by rewrite divpE lead_coefC unitr1 Ring.rdivp1 expr1n invr1 scale1r. 
+by rewrite divpE lead_coefC unitr1 Ring.rdivp1 expr1n invr1 scale1r.
 Qed.
 
 Lemma modp0 p : p %% 0 = p.
@@ -1225,7 +1225,7 @@ rewrite /dvdp; apply/idPn=> m_nz.
 have: p1 * q != 0 by rewrite -E1 -mul_polyC mulf_neq0 // polyC_eq0.
 rewrite mulf_eq0; case/norP=> p1_nz q_nz.
 have := (ltn_modp p q); rewrite q_nz -(size_scale (p %% q) cn0) E1.
-by rewrite  size_mul // polySpred // ltnNge leq_addl.
+by rewrite size_mul // polySpred // ltnNge leq_addl.
 Qed.
 
 Lemma dvdpp d : d %| d.
@@ -1258,7 +1258,7 @@ Hint Resolve dvdp_mull dvdp_mulr.
 Lemma dvdp_mul d1 d2 m1 m2 : d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2.
 Proof.
 case: (eqVneq d1 0) => [-> |d1n0]; first by move/dvd0pP->; rewrite !mul0r dvdpp.
-case: (eqVneq d2 0) => [-> |d2n0]; first by move => _ /dvd0pP ->; rewrite !mulr0.
+case: (eqVneq d2 0) => [-> |d2n0]; first by move=> _ /dvd0pP ->; rewrite !mulr0.
 rewrite dvdp_eq; set c1 := _ ^+ _; set q1 := _ %/ _; move/eqP=> Hq1.
 rewrite dvdp_eq; set c2 := _ ^+ _; set q2 := _ %/ _; move/eqP=> Hq2.
 apply: (@eq_dvdp (c1 * c2) (q1 * q2)).
@@ -1341,11 +1341,11 @@ Proof. by apply: dvdp_mull; apply: dvdpp. Qed.
 
 Lemma dvdp_mul2r r p q : r != 0 -> (p * r %| q * r) = (p %| q).
 Proof.
-move => nzr.
+move=> nzr.
 case: (eqVneq p 0) => [-> | pn0].
   by rewrite mul0r !dvd0p mulf_eq0 (negPf nzr) orbF.
 case: (eqVneq q 0) => [-> | qn0]; first by rewrite mul0r !dvdp0.
-apply/idP/idP; last by move => ?; rewrite dvdp_mul ?dvdpp.
+apply/idP/idP; last by move=> ?; rewrite dvdp_mul ?dvdpp.
 rewrite dvdp_eq; set c := _ ^+ _; set x := _ %/ _; move/eqP=> Hx.
 apply: (@eq_dvdp c x).
   by rewrite expf_neq0 // lead_coef_eq0 mulf_neq0.
@@ -1388,7 +1388,7 @@ Lemma dvdp_exp_sub p q k l: p != 0 ->
   (p ^+ k %| q * p ^+ l) = (p ^+ (k - l) %| q).
 Proof.
 move=> pn0; case: (leqP k l)=> hkl.
-  move:(hkl); rewrite -subn_eq0; move/eqP->; rewrite expr0 dvd1p.
+  move: (hkl); rewrite -subn_eq0; move/eqP->; rewrite expr0 dvd1p.
   apply: dvdp_mull; case: (ltnP 1%N (size p)) => sp.
     by rewrite dvdp_Pexp2l.
   move: sp; case esp: (size p) => [|sp].
@@ -1532,7 +1532,7 @@ have n0q : q != 0.
   by case abs: (q == 0) => //; move: hq; rewrite (eqP abs) eqp01.
 rewrite -size_poly_eq1 eqn_leq -{1}(eqP sizeq) dvdp_leq //=.
 case p0 : (size p == 0%N); last by rewrite neq0_lt0n.
-by move: dpq;  rewrite size_poly_eq0 in p0; rewrite (eqP p0) dvd0p (negbTE n0q).
+by move: dpq; rewrite size_poly_eq0 in p0; rewrite (eqP p0) dvd0p (negbTE n0q).
 Qed.
 
 Lemma eqp_dvdr q p d: p %= q -> d %| p = (d %| q).
@@ -1558,10 +1558,10 @@ Lemma dvdp_opp d p : d %| (- p) = (d %| p).
 Proof. by apply: eqp_dvdr; rewrite -scaleN1r eqp_scale ?oppr_eq0 ?oner_eq0. Qed.
 
 Lemma eqp_mul2r r p q : r != 0 -> (p * r %= q * r) = (p %= q).
-Proof. by move => nz_r; rewrite /eqp !dvdp_mul2r. Qed.
+Proof. by move=> nz_r; rewrite /eqp !dvdp_mul2r. Qed.
 
 Lemma eqp_mul2l r p q: r != 0 -> (r * p %= r * q) = (p %= q).
-Proof. by move => nz_r; rewrite /eqp !dvdp_mul2l. Qed.
+Proof. by move=> nz_r; rewrite /eqp !dvdp_mul2l. Qed.
 
 Lemma eqp_mull r p q: (q %= r) -> (p * q %= p * r).
 Proof.
@@ -1570,7 +1570,7 @@ by rewrite scalerAr e -scalerAr.
 Qed.
 
 Lemma eqp_mulr q p r : (p %= q) -> (p * r %= q * r).
-Proof. by move=>  epq; rewrite ![_ * r]mulrC eqp_mull. Qed.
+Proof. by move=> epq; rewrite ![_ * r]mulrC eqp_mull. Qed.
 
 Lemma eqp_exp  p q k : p %= q -> p ^+ k %= q ^+ k.
 Proof.
@@ -1598,7 +1598,7 @@ case (q =P 0)=> [->|]; [|move/eqP => Hq].
 case (p =P 0)=> [->|]; [|move/eqP => Hp].
   by rewrite size_poly0 eq_sym size_poly_eq0; move/eqP->; rewrite eqpxx.
 move: pq; rewrite dvdp_eq; set c := _ ^+ _; set x := _ %/ _; move/eqP=> eqpq.
-move:(eqpq); move/(congr1 (size \o (@polyseq R)))=> /=.
+move: (eqpq); move/(congr1 (size \o (@polyseq R)))=> /=.
 have cn0 : c != 0 by  rewrite expf_neq0 // lead_coef_eq0.
 rewrite (@eqp_size _ q); last  by apply: eqp_scale.
 rewrite size_mul ?p0 // => [-> HH|]; last first.
@@ -1608,7 +1608,7 @@ suff: size x == 1%N.
   case/size_poly1P=> y H1y H2y.
   by apply/eqpP; exists (y, c); rewrite ?H1y // eqpq H2y mul_polyC.
 case: (size p) HH (size_poly_eq0 p)=> [|n]; first by case: eqP Hp.
-by rewrite addnS -add1n eqn_add2r;move/eqP->.
+by rewrite addnS -add1n eqn_add2r; move/eqP->.
 Qed.
 
 Lemma eqp_root p q : p %= q -> root p =1 root q.
@@ -1809,7 +1809,7 @@ Proof.
 case: (eqVneq n 0) => [-> | nn0]; first by rewrite gcd0p mulr0 eqpxx.
 case: (eqVneq m 0) => [-> | mn0]; first by rewrite mul0r gcdp0 eqpxx.
 rewrite gcdpE modp_mull gcd0p size_mul //; case: ifP; first by rewrite eqpxx.
-rewrite  (polySpred mn0) addSn /= -{1}[size n]add0n ltn_add2r; move/negbT.
+rewrite (polySpred mn0) addSn /= -{1}[size n]add0n ltn_add2r; move/negbT.
 rewrite -ltnNge prednK ?size_poly_gt0 // leq_eqVlt ltnS leqn0 size_poly_eq0.
 rewrite (negPf mn0) orbF; case/size_poly1P=> c cn0 -> {mn0 m}; rewrite mul_polyC.
 suff -> : n %% (c *: n) = 0 by rewrite gcd0p; apply: eqp_scale.
@@ -2042,7 +2042,7 @@ Proof.
 elim=> [|k ihk] p q /= qn0; first by rewrite leqn0 size_poly_eq0 (negPf qn0).
 move=> sqSn qsp; case: (eqVneq q 0)=> q0; first by rewrite q0 eqxx in qn0.
 rewrite (negPf qn0).
-have sp : size p > 0 by apply: leq_trans qsp; rewrite  size_poly_gt0.
+have sp : size p > 0 by apply: leq_trans qsp; rewrite size_poly_gt0.
 case: (eqVneq (p %% q) 0) => [r0 | rn0] /=.
   rewrite r0 /egcdp_rec; case: k ihk sqSn => [|n] ihn sqSn /=.
     rewrite !scaler0 !mul0r subr0 add0r mul1r size_poly0 size_poly1.
@@ -2063,13 +2063,13 @@ rewrite gcdpE ltnNge qsp //= (eqp_ltrans (gcdpC _ _)); split; last first.
     rewrite mul0r size_opp size_poly0 maxn0; apply: leq_trans ihn'1 _.
     exact: leq_modp.
   case: (eqVneq (p %/ q) 0)=> [-> | qqn0].
-    rewrite mulr0 size_opp size_poly0 maxn0;  apply: leq_trans ihn'1 _.
+    rewrite mulr0 size_opp size_poly0 maxn0; apply: leq_trans ihn'1 _.
     exact: leq_modp.
   rewrite geq_max (leq_trans ihn'1) ?leq_modp //= size_opp size_mul //.
   move: (ihn'2); rewrite -(leq_add2r (size (p %/ q))).
   have : size v + size (p %/ q) > 0 by rewrite addn_gt0 size_poly_gt0 vn0.
   have : size q + size (p %/ q) > 0 by rewrite addn_gt0 size_poly_gt0 qn0.
-  do 2! move/prednK=> {1}<-; rewrite ltnS => h; apply: leq_trans h _.
+  do 2!move/prednK=> {1}<-; rewrite ltnS => h; apply: leq_trans h _.
   rewrite size_divp // addnBA; last by apply: leq_trans qsp; apply: leq_pred.
   rewrite addnC -addnBA ?leq_pred //; move: qn0; rewrite -size_poly_eq0 -lt0n.
   by move/prednK=> {1}<-; rewrite subSnn addn1.
@@ -2107,10 +2107,10 @@ Qed.
 Lemma Bezout_coprimepP : forall p q,
   reflect (exists u, u.1 * p + u.2 * q %= 1) (coprimep p q).
 Proof.
-move=> p q; rewrite -gcdp_eqp1; apply:(iffP idP)=> [g1|].
+move=> p q; rewrite -gcdp_eqp1; apply: (iffP idP)=> [g1|].
   by case: (Bezoutp p q) => [[u v] Puv]; exists (u, v); apply: eqp_trans g1.
-case=>[[u v]]; rewrite eqp_sym=> Puv; rewrite /eqp  (eqp_dvdr _ Puv).
-by rewrite  dvdp_addr dvdp_mull ?dvdp_gcdl ?dvdp_gcdr //= dvd1p.
+case=> [[u v]]; rewrite eqp_sym=> Puv; rewrite /eqp  (eqp_dvdr _ Puv).
+by rewrite dvdp_addr dvdp_mull ?dvdp_gcdl ?dvdp_gcdr //= dvd1p.
 Qed.
 
 Lemma coprimep_root p q x : coprimep p q -> root p x -> q.[x] != 0.
@@ -2126,7 +2126,7 @@ Qed.
 Lemma Gauss_dvdpl p q d: coprimep d q -> (d %| p * q) = (d %| p).
 Proof.
 move/Bezout_coprimepP=>[[u v] Puv]; apply/idP/idP; last exact: dvdp_mulr.
-move:Puv; move/(eqp_mull p); rewrite mulr1 mulrDr eqp_sym=> peq dpq.
+move: Puv; move/(eqp_mull p); rewrite mulr1 mulrDr eqp_sym=> peq dpq.
 rewrite (eqp_dvdr _  peq) dvdp_addr; first by rewrite mulrA mulrAC dvdp_mulr.
 by rewrite mulrA dvdp_mull ?dvdpp.
 Qed.
@@ -2138,7 +2138,7 @@ Proof. by rewrite mulrC; apply: Gauss_dvdpl. Qed.
 Lemma Gauss_dvdp m n p : coprimep m n -> (m * n %| p) = (m %| p) && (n %| p).
 Proof.
 case: (eqVneq m 0) => [-> | mn0].
-  by rewrite coprime0p;  move/eqp_dvdl->; rewrite !mul0r dvd0p dvd1p andbT.
+  by rewrite coprime0p; move/eqp_dvdl->; rewrite !mul0r dvd0p dvd1p andbT.
 case: (eqVneq n 0) => [-> | nn0].
   by rewrite coprimep0; move/eqp_dvdl->; rewrite !mulr0 dvd1p.
 move=> hc; apply/idP/idP.
@@ -2149,7 +2149,7 @@ case/andP => dmp dnp; move: (dnp); rewrite dvdp_eq.
 set c2 := _ ^+ _; set q2 := _ %/ _; move/eqP=> e2.
 have := (sym_eq (Gauss_dvdpl q2 hc)); rewrite -e2.
 have -> : m %| c2 *: p by rewrite -mul_polyC dvdp_mull.
-rewrite dvdp_eq;  set c3 := _ ^+ _; set q3 := _ %/ _; move/eqP=> e3.
+rewrite dvdp_eq; set c3 := _ ^+ _; set q3 := _ %/ _; move/eqP=> e3.
 apply: (@eq_dvdp (c3 * c2) q3).
   by rewrite mulf_neq0 // expf_neq0 // lead_coef_eq0.
 by rewrite mulrA -e3 -scalerAl -e2 scalerA.
@@ -2170,7 +2170,7 @@ Proof. by move=> co_pn; rewrite mulrC Gauss_gcdpr. Qed.
 Lemma coprimep_mulr p q r : coprimep p (q * r) = (coprimep p q && coprimep p r).
 Proof.
 apply/coprimepP/andP=> [hp | [/coprimepP-hq hr]].
-  by split; apply/coprimepP=> d dp dq; rewrite hp //; 
+  by split; apply/coprimepP=> d dp dq; rewrite hp //;
      [apply/dvdp_mulr | apply/dvdp_mull].
 move=> d dp dqr; move/(_ _ dp) in hq.
 rewrite Gauss_dvdpl in dqr; first exact: hq.
@@ -2309,7 +2309,7 @@ have /size_poly1P [c cn0 em'] : size m' == 1%N.
     by rewrite (negPf mn0) (negPf c2n0).
   have := (hc _ (dvdpp _) hd); rewrite -size_poly_eq1.
   rewrite polySpred; last by rewrite expf_eq0 negb_and m'_n0 orbT.
-  rewrite size_exp eqSS muln_eq0;  move: k_gt0; rewrite lt0n; move/negPf->.
+  rewrite size_exp eqSS muln_eq0; move: k_gt0; rewrite lt0n; move/negPf->.
   by rewrite orbF -{2}(@prednK (size m')) ?lt0n // size_poly_eq0.
 rewrite -(@dvdp_scalel c2) // def_m em' mul_polyC dvdp_scalel //.
 by rewrite -(@dvdp_scaler c1) // def_n dvdp_mull.
@@ -2387,7 +2387,7 @@ case dpq: (d %| gcdp p q).
   move: (dpq); rewrite dvdp_gcd dp /= => dq; apply: dvdUp; move: cdq.
   apply: contraLR=> nd1; apply/coprimepPn; last first.
     by exists d; rewrite dvdp_gcd dvdpp dq nd1.
-  move/negP: p0; move/negP; apply: contra=> d0; move:dp; rewrite (eqP d0).
+  move/negP: p0; move/negP; apply: contra=> d0; move: dp; rewrite (eqP d0).
   by rewrite dvd0p.
 move: (dp); apply: contraLR=> ndp'.
 rewrite (@eqp_dvdr ((lead_coef (gcdp p q) ^+ scalp p (gcdp p q))*:p)).
@@ -2409,7 +2409,7 @@ move=> p0 sd; apply/idP/idP.
   case: gdcopP=> r rp crq maxr dr; move/negPf: (p0)=> p0f.
   rewrite (dvdp_trans dr) //=.
   move: crq; apply: contraL=> dq; rewrite p0f orbF; apply/coprimepPn.
-    by move:p0; apply: contra=> r0; move: rp; rewrite (eqP r0) dvd0p.
+    by move: p0; apply: contra=> r0; move: rp; rewrite (eqP r0) dvd0p.
   by exists d; rewrite dvdp_gcd dr dq -size_poly_eq1 sd.
 case/andP=> dp dq; case: gdcopP=> r rp crq maxr; apply: maxr=> //.
 apply/coprimepP=> x xd xq.
@@ -2472,7 +2472,7 @@ Lemma modp_XsubC p c : p %% ('X - c%:P) = p.[c]%:P.
 Proof.
 have: root (p - p.[c]%:P) c by rewrite /root !hornerE subrr.
 case/factor_theorem=> q /(canRL (subrK _)) Dp; rewrite modpE /= lead_coefXsubC.
-rewrite  GRing.unitr1 expr1n invr1 scale1r {1}Dp.
+rewrite GRing.unitr1 expr1n invr1 scale1r {1}Dp.
 rewrite RingMonic.rmodp_addl_mul_small // ?monicXsubC // size_XsubC size_polyC.
 by case: (p.[c] == 0).
 Qed.
@@ -2735,7 +2735,7 @@ Qed.
 Lemma mulpK q : (q * d) %/ d = q.
 Proof.
 case/edivpP: (sym_eq (addr0 (q * d))); rewrite // size_poly0 size_poly_gt0.
-by rewrite  -lead_coef_eq0; apply: contraTneq ulcd => ->; rewrite unitr0.
+by rewrite -lead_coef_eq0; apply: contraTneq ulcd => ->; rewrite unitr0.
 Qed.
 
 Lemma mulKp q : (d * q) %/ d = q.
@@ -2785,7 +2785,7 @@ by rewrite -lead_coef_eq0; apply: contraTneq ulcd => ->; rewrite unitr0.
 Qed.
 
 Lemma dvdp_eq_mul p q : d %| p -> (p == q * d) = (p %/ d == q).
-Proof. by move=>dv_d_p; rewrite eq_sym -dvdp_eq_div // eq_sym. Qed.
+Proof. by move=> dv_d_p; rewrite eq_sym -dvdp_eq_div // eq_sym. Qed.
 
 Lemma divp_mulA p q : d %| q -> p * (q %/ d) = p * q %/ d.
 Proof.
@@ -3206,7 +3206,7 @@ Qed.
 
 Lemma edivp_eq d q r : size r < size d -> edivp (q * d + r) d = (0%N, q, r).
 Proof.
-move=> srd; apply: Idomain.edivp_eq ; rewrite // unitfE lead_coef_eq0.
+move=> srd; apply: Idomain.edivp_eq; rewrite // unitfE lead_coef_eq0.
 by rewrite -size_poly_gt0; apply: leq_trans srd.
 Qed.
 
@@ -3228,8 +3228,8 @@ Qed.
 Lemma Bezout_eq1_coprimepP : forall p q,
   reflect (exists u, u.1 * p + u.2 * q = 1) (coprimep p q).
 Proof.
-move=> p q; apply:(iffP idP)=> [hpq|]; last first.
-  by case=>[[u v]] /= e; apply/Bezout_coprimepP; exists (u, v); rewrite e eqpxx.
+move=> p q; apply: (iffP idP)=> [hpq|]; last first.
+  by case=> [[u v]] /= e; apply/Bezout_coprimepP; exists (u, v); rewrite e eqpxx.
 case/Bezout_coprimepP: hpq => [[u v]] /=.
 case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0] e.
 exists (c2^-1  *: (c1 *: u), c2^-1 *: (c1 *: v)); rewrite /=  -!scalerAl.
@@ -3298,7 +3298,7 @@ Proof.
 rewrite /rdivp /rscalp /rmodp !unlock map_poly_eq0 size_map_poly.
 case: eqP; rewrite /= -(rmorph0 (map_poly_rmorphism f)) //; move/eqP=> q_nz.
 move: (size a) => m; elim: m 0%N 0 a => [|m IHm] qq r a /=.
-  rewrite  -!mul_polyC  !size_map_poly !lead_coef_map // -(map_polyXn f).
+  rewrite -!mul_polyC  !size_map_poly !lead_coef_map // -(map_polyXn f).
   by rewrite -!(map_polyC f) -!rmorphM -rmorphB -rmorphD; case: (_ < _).
 rewrite -!mul_polyC !size_map_poly !lead_coef_map // -(map_polyXn f).
 by rewrite -!(map_polyC f) -!rmorphM -rmorphB -rmorphD /= IHm; case: (_ < _).
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index d004748..e837ed2 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -32,7 +32,7 @@ Local Open Scope ring_scope.
 Local Notation sgr := Num.sg.
 
 Record rat : Set := Rat {
-  valq : (int * int) ;
+  valq : (int * int);
   _ : (0 < valq.2) && coprime `|valq.1| `|valq.2|
 }.
 
@@ -73,7 +73,7 @@ Lemma coprime_num_den x : coprime `|numq x| `|denq x|.
 Proof. by rewrite /numq /denq; case: x=> [[a b] /= /andP []]. Qed.
 
 Fact RatK x P : @Rat (numq x, denq x) P = x.
-Proof. by move:x P => [[a b] P'] P; apply: val_inj. Qed.
+Proof. by move: x P => [[a b] P'] P; apply: val_inj. Qed.
 
 Fact fracq_subproof : forall x : int * int,
   let n :=
@@ -100,8 +100,8 @@ Proof. by apply: val_inj; rewrite /= gcdn1 !divn1 abszE mulr_sign_norm. Qed.
 
 Fact valqK x : fracq (valq x) = x.
 Proof.
-move:x => [[n d] /= Pnd]; apply: val_inj=> /=.
-move: Pnd; rewrite /coprime /fracq /=; case/andP=> hd; move/eqP=> hnd.
+move: x => [[n d] /= Pnd]; apply: val_inj=> /=.
+move: Pnd; rewrite /coprime /fracq /= => -/andP[] hd -/eqP hnd.
 by rewrite ltr_gtF ?gtr_eqF //= hnd !divn1 mulz_sign_abs abszE gtr0_norm.
 Qed.
 
@@ -407,7 +407,7 @@ Proof. by rewrite -ratzE /ratz rat_eqE /numq /denq /= mulr0 eqxx andbT. Qed.
 (* fracq should never appear, its canonical form is _%:Q / _%:Q *)
 Lemma fracqE x : fracq x = x.1%:Q / x.2%:Q.
 Proof.
-move:x => [m n] /=.
+move: x => [m n] /=.
 case n0: (n == 0); first by rewrite (eqP n0) fracq0 rat0 invr0 mulr0.
 rewrite -[m%:Q]valqK -[n%:Q]valqK.
 rewrite [_^-1]invq_frac ?(denq_neq0, numq_eq0, n0, intq_eq0) //.
@@ -426,7 +426,7 @@ CoInductive divq_spec (n d : int) : int -> int -> rat -> Type :=
 Lemma divqP n d : divq_spec n d n d (n%:Q / d%:Q).
 Proof.
 set x := (n, d); rewrite -[n]/x.1 -[d]/x.2 -fracqE.
-by case: fracqP => [_|k fx k_neq0] /=; constructor. 
+by case: fracqP => [_|k fx k_neq0] /=; constructor.
 Qed.
 
 Lemma divq_eq (nx dx ny dy : rat) :
@@ -466,7 +466,8 @@ Qed.
 
 Lemma denqVz (i : int) : i != 0 -> denq (i%:~R^-1) = `|i|.
 Proof.
-by move=> h; rewrite -div1r -[1]/(1%:~R) coprimeq_den /= ?coprime1n // (negPf h).
+move=> h; rewrite -div1r -[1]/(1%:~R).
+by rewrite coprimeq_den /= ?coprime1n // (negPf h).
 Qed.
 
 Lemma numqE x : (numq x)%:~R = x * (denq x)%:~R.
@@ -657,7 +658,7 @@ Qed.
 
 Fact Qnat_semiring_closed : semiring_closed Qnat.
 Proof.
-do 2?split; move => // x y; rewrite !Qnat_def => /andP[xQ hx] /andP[yQ hy].
+do 2?split; move=> // x y; rewrite !Qnat_def => /andP[xQ hx] /andP[yQ hy].
   by rewrite rpredD // addr_ge0.
 by rewrite rpredM // mulr_ge0.
 Qed.
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 15bce96..9a0314e 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -756,7 +756,7 @@ Lemma eqr_opp x y : (- x == - y) = (x == y).
 Proof. exact: can_eq opprK x y. Qed.
 
 Lemma eqr_oppLR x y : (- x == y) = (x == - y).
-Proof. exact: inv_eq opprK x y. Qed. 
+Proof. exact: inv_eq opprK x y. Qed.
 
 Lemma mulr0n x : x *+ 0 = 0. Proof. by []. Qed.
 Lemma mulr1n x : x *+ 1 = x. Proof. by []. Qed.
@@ -1234,7 +1234,7 @@ rewrite exprS {}IHn /= mulrDl !big_distrr /= big_ord_recl mulr1 subn0.
 rewrite !big_ord_recr /= !binn !subnn !mul1r !subn0 bin0 !exprS -addrA.
 congr (_ + _); rewrite addrA -big_split /=; congr (_ + _).
 apply: eq_bigr => i _; rewrite !mulrnAr !mulrA -exprS -subSn ?(valP i) //.
-by rewrite  subSS (commrX _ (commr_sym cxy)) -mulrA -exprS -mulrnDr.
+by rewrite subSS (commrX _ (commr_sym cxy)) -mulrA -exprS -mulrnDr.
 Qed.
 
 Lemma exprBn_comm x y n (cxy : comm x y) :
@@ -2612,7 +2612,7 @@ Section ClassDef.
 Variable R : ringType.
 
 Record class_of (T : Type) : Type := Class {
-  base : Lalgebra.class_of R T; 
+  base : Lalgebra.class_of R T;
   mixin : axiom (Lalgebra.Pack _ base T)
 }.
 Local Coercion base : class_of >-> Lalgebra.class_of.
@@ -2682,7 +2682,7 @@ Lemma mulr_algr a x : x * a%:A = a *: x.
 Proof. by rewrite -scalerAr mulr1. Qed.
 
 Lemma exprZn k x n : (k *: x) ^+ n = k ^+ n *: x ^+ n.
-Proof. 
+Proof.
 elim: n => [|n IHn]; first by rewrite !expr0 scale1r.
 by rewrite !exprS IHn -scalerA scalerAr scalerAl.
 Qed.
@@ -3124,7 +3124,7 @@ Section ClassDef.
 Variable R : ringType.
 
 Record class_of (T : Type) : Type := Class {
-  base : Algebra.class_of R T; 
+  base : Algebra.class_of R T;
   mixin : GRing.UnitRing.mixin_of (Ring.Pack base T)
 }.
 Definition base2 R m := UnitRing.Class (@mixin R m).
@@ -3627,7 +3627,7 @@ End LmodPred.
 
 Section UnitRingPred.
 
-Variable R : unitRingType. 
+Variable R : unitRingType.
 
 Section Div.
 
@@ -4247,7 +4247,7 @@ Proof. by move=> /= -> -> ->. Qed.
 
 Lemma eval_If e :
   let ev := qf_eval e in ev If = (if ev pred_f then ev then_f else ev else_f).
-Proof. by rewrite /=; case: ifP => _; rewrite ?orbF. Qed. 
+Proof. by rewrite /=; case: ifP => _; rewrite ?orbF. Qed.
 
 End If.
 
@@ -6011,7 +6011,7 @@ Section FinFunRing.
 Variable (aT : finType) (R : ringType) (a : aT).
 
 Definition ffun_one : {ffun aT -> R} := [ffun => 1].
-Definition ffun_mul (f g : {ffun aT -> R}) := [ffun x => f x * g x]. 
+Definition ffun_mul (f g : {ffun aT -> R}) := [ffun x => f x * g x].
 
 Fact ffun_mulA : associative ffun_mul.
 Proof. by move=> f1 f2 f3; apply/ffunP=> i; rewrite !ffunE mulrA. Qed.
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index eb66940..e6c4ca6 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -120,7 +120,7 @@ Lemma int_rect (P : int -> Type) :
   -> (forall n : nat, P (- n) -> P (- (n.+1)))
   -> forall n : int, P n.
 Proof.
-by move=> P0 hPp hPn []; elim=> [|n ihn]//; do? [apply: hPn | apply: hPp].
+by move=> P0 hPp hPn []; elim=> [|n ihn]//; do ?[apply: hPn | apply: hPp].
 Qed.
 
 Definition int_rec := int_rect.
@@ -210,7 +210,7 @@ Lemma int_rect (P : int -> Type) :
   -> (forall n : nat, P (- (n%:Z)) -> P (- (n.+1%N%:Z)))
   -> forall n : int, P n.
 Proof.
-by move=> P0 hPp hPn []; elim=> [|n ihn]//; do? [apply: hPn | apply: hPp].
+by move=> P0 hPp hPn []; elim=> [|n ihn]//; do ?[apply: hPn | apply: hPp].
 Qed.
 
 Definition int_rec := int_rect.
@@ -546,7 +546,7 @@ case: (leqP m n)=> hmn; rewrite /intmul //=.
   rewrite -{2}[n](@subnKC m)// mulrnDr opprD addrA subrr sub0r.
   by case hdmn: (_ - _)%N=> [|dmn] /=; first by rewrite mulr0n oppr0.
 have hnm := ltnW hmn.
-rewrite  -{2}[m](@subnKC n)// mulrnDr addrAC subrr add0r.
+rewrite -{2}[m](@subnKC n)// mulrnDr addrAC subrr add0r.
 by rewrite subzn.
 Qed.
 
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index b7a9052..c4865ca 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -204,7 +204,7 @@ Proof.
 have r2vP r: {v | v2r v = r}.
   by apply: sig_eqW; have [v _ vK] := v2r_bij; exists (v r).
 by exists (fun r => sval (r2vP r)) => r; case: (r2vP r).
-Qed. 
+Qed.
 Definition r2v := sval r2v_subproof.
 
 Lemma r2vK : cancel r2v v2r.   Proof. exact: (svalP r2v_subproof). Qed.
@@ -721,7 +721,7 @@ Lemma dimvS U V : (U <= V)%VS -> \dim U <= \dim V.
 Proof. exact: mxrankS. Qed.
 
 Lemma dimv_leqif_sup U V : (U <= V)%VS -> \dim U <= \dim V ?= iff (V <= U)%VS.
-Proof. exact: mxrank_leqif_sup. Qed. 
+Proof. exact: mxrank_leqif_sup. Qed.
 
 Lemma dimv_leqif_eq U V : (U <= V)%VS -> \dim U <= \dim V ?= iff (U == V).
 Proof. by rewrite eqEsubv; apply: mxrank_leqif_eq. Qed.
@@ -939,7 +939,7 @@ Lemma span_subvP {X U} : reflect {subset X <= U} (<<X>> <= U)%VS.
 Proof.
 rewrite /subV [@span _ _]unlock genmxE.
 apply: (iffP row_subP) => /= [sXU | sXU i].
-  by move=>  _ /seq_tnthP[i ->]; have:= sXU i; rewrite rowK memvK.
+  by move=> _ /seq_tnthP[i ->]; have:= sXU i; rewrite rowK memvK.
 by rewrite rowK -memvK sXU ?mem_tnth.
 Qed.
 
@@ -1005,7 +1005,7 @@ Lemma seq1_free v : free [:: v] = (v != 0).
 Proof. by rewrite /free span_seq1 dim_vline; case: (~~ _). Qed.
  
 Lemma perm_free X Y : perm_eq X Y -> free X = free Y.
-Proof. 
+Proof.
 by move=> eqX; rewrite /free (perm_eq_size eqX) (eq_span (perm_eq_mem eqX)).
 Qed.
 
@@ -1202,7 +1202,7 @@ Lemma bigcat_free :
     directv (\sum_(i | P i) <<Xs i>>) -> 
   (forall i, P i -> free (Xs i)) -> free (\big[cat/[::]]_(i | P i) Xs i).
 Proof.
-rewrite /free directvE /= span_bigcat => /directvP-> /= freeXs. 
+rewrite /free directvE /= span_bigcat => /directvP-> /= freeXs.
 rewrite (big_morph _ (@size_cat _) (erefl _)) /=.
 by apply/eqP/eq_bigr=> i /freeXs/eqP.
 Qed.
@@ -1534,7 +1534,7 @@ Qed.
 Lemma limg_lfunVK f : {in limg f, cancel f^-1%VF f}.
 Proof. by move=> _ /memv_imgP[u _ ->]; rewrite -!comp_lfunE inv_lfun_def. Qed.
 
-Lemma lkerE f U : (U <= lker f)%VS = (f @: U == 0)%VS. 
+Lemma lkerE f U : (U <= lker f)%VS = (f @: U == 0)%VS.
 Proof.
 rewrite unlock -dimv_eq0 /dimv /subsetv !genmxE mxrank_eq0.
 by rewrite (sameP sub_kermxP eqP).
@@ -1550,7 +1550,7 @@ Lemma eqlfun_inP V f g : reflect {in V, f =1 g} (V <= lker (f - g))%VS.
 Proof. by apply: (iffP subvP) => E x /E/eqlfunP. Qed.
 
 Lemma limg_ker_compl f U : (f @: (U :\: lker f) = f @: U)%VS.
-Proof. 
+Proof.
 rewrite -{2}(addv_diff_cap U (lker f)) limg_add; apply/esym/addv_idPl.
 by rewrite (subv_trans _ (sub0v _)) // subv0 -lkerE capvSr.
 Qed.
@@ -1825,7 +1825,7 @@ Lemma addv_pi2_proj U V w (pi2 := addv_pi2 U V) : pi2 (pi2 w) = pi2 w.
 Proof. by rewrite addv_pi2_id ?memv_pi2. Qed.
 
 Lemma addv_pi1_pi2 U V w :
-  w \in (U + V)%VS -> addv_pi1 U V w + addv_pi2 U V w = w. 
+  w \in (U + V)%VS -> addv_pi1 U V w + addv_pi2 U V w = w.
 Proof. by rewrite -addv_diff; apply: daddv_pi_add; apply: capv_diff. Qed.
 
 Section Sumv_Pi.