Merge pull request #607 from pi8027/distr-suffixes

Switch from long suffixes to short suffixes

6 files changed, 47 insertions, 52 deletions

diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index d8ad524..a950ecc 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -160,7 +160,7 @@ have [n ub_n]: {n | forall y, root q y -> `|y| < n}.
   have [n1 ub_n1] := monic_Cauchy_bound mon_q.
   have /monic_Cauchy_bound[n2 ub_n2]: (-1) ^+ d *: (q \Po - 'X) \is monic.
     rewrite monicE lead_coefZ lead_coef_comp ?size_opp ?size_polyX // -/d.
-    by rewrite lead_coef_opp lead_coefX (monicP mon_q) (mulrC 1) signrMK.
+    by rewrite lead_coefN lead_coefX (monicP mon_q) (mulrC 1) signrMK.
   exists (Num.max n1 n2) => y; rewrite ltNge ler_normr !leUx rootE.
   apply: contraL => /orP[]/andP[] => [/ub_n1/gt_eqF->// | _ /ub_n2/gt_eqF].
   by rewrite hornerZ horner_comp !hornerE opprK mulf_eq0 signr_eq0 => /= ->.
@@ -171,7 +171,7 @@ right=> [[y Dx]]; case: xa'x; exists y => //.
 have{x Dx qx0} qy0: root q y by rewrite Dx fmorph_root in qx0.
 have /dvdzP[b Da]: (denq y %| a)%Z.
   have /Gauss_dvdzl <-: coprimez (denq y) (numq y ^+ d).
-    by rewrite coprimez_sym coprimez_expl //; apply: coprime_num_den.
+    by rewrite coprimez_sym coprimezXl //; apply: coprime_num_den.
   pose p1 : {poly int} := a *: 'X^d - p.
   have Dp1: p1 ^ intr = a%:~R *: ('X^d - q).
     by rewrite rmorphB linearZ /= map_polyXn scalerBr Dq scalerKV ?intr_eq0.
@@ -231,7 +231,7 @@ without loss mon_q: q nCq q_dv_p / q \is monic.
   move=> IHq; pose a := lead_coef q; pose q1 := a^-1 *: q.
   have nz_a: a != 0 by rewrite lead_coef_eq0 (dvdpN0 q_dv_p) ?monic_neq0.
   have /IHq IHq1: q1 \is monic by rewrite monicE lead_coefZ mulVf.
-  by rewrite -IHq1 ?size_scale ?dvdp_scalel ?invr_eq0.
+  by rewrite -IHq1 ?size_scale ?dvdpZl ?invr_eq0.
 without loss{nCq} qx0: q mon_q q_dv_p / root (q ^ FtoL) x.
   have /dvdpP[q1 Dp] := q_dv_p; rewrite DpI Dp rmorphM rootM -implyNb in pIx0.
   have mon_q1: q1 \is monic by rewrite Dp monicMr in mon_p.
@@ -515,7 +515,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}.
   have ab_le m n: (m <= n)%N -> (ab_ n).2 \in Iab_ m.
     move/subnKC=> <-; move: {n}(n - m)%N => n; rewrite /ab_.
     have /(findP m)[/(findP n)[[_ _]]] := xab0.
-    rewrite /find -iter_add -!/(find _ _) -!/(ab_ _) addnC !inE.
+    rewrite /find -iterD -!/(find _ _) -!/(ab_ _) addnC !inE.
     by move: (ab_ _) => /= ab_mn le_ab_mn [/le_trans->].
   pose lt v w := 0 < nlim (w - v) (n_ (w - v)).
   have posN v: lt 0 (- v) = lt v 0 by rewrite /lt subr0 add0r.
@@ -723,7 +723,7 @@ have /all_sig[n_ FTA] z: {n | z \in sQ (z_ n)}.
     have mon_p: p \is monic.
       have mon_pw: pw \is monic := monic_minPoly _ _.
       rewrite map_monic mulNr -mulrN monicMl // monicE.
-      rewrite !(lead_coef_opp, lead_coef_comp) ?size_opp ?size_polyX //.
+      rewrite !(lead_coefN, lead_coef_comp) ?size_opp ?size_polyX //.
       by rewrite lead_coefX sz_pw -signr_odd odd_2'nat oddPG mulrN1 opprK.
     have Dp0: p.[0] = - ofQ t pw.[0] ^+ 2.
       rewrite -(rmorph0 (ofQ t)) horner_map hornerM rmorphM.
diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v
index a6f7514..266788c 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -200,7 +200,7 @@ Lemma eval_sumpT (p q : polyF) (e : seq F) :
 Proof.
 elim: p q => [|a p Hp] q /=; first by rewrite add0r.
 case: q => [|b q] /=; first by rewrite addr0.
-rewrite Hp mulrDl -!addrA; congr (_ + _); rewrite polyC_add addrC -addrA.
+rewrite Hp mulrDl -!addrA; congr (_ + _); rewrite polyCD addrC -addrA.
 by congr (_ + _); rewrite addrC.
 Qed.
 
@@ -220,15 +220,12 @@ Lemma eval_mulpT (p q : polyF) (e : seq F) :
 Proof.
 elim: p q=> [|a p Hp] q /=; first by rewrite mul0r.
 rewrite eval_sumpT /= Hp addr0 mulrDl addrC mulrAC; congr (_ + _).
-elim: q=> [|b q Hq] /=; first by rewrite mulr0.
-by rewrite Hq polyC_mul mulrDr mulrA.
+by elim: q=> [|b q Hq] /=; rewrite ?mulr0 // Hq polyCM mulrDr mulrA.
 Qed.
 
 Lemma rpoly_map_mul (t : tF) (p : polyF) (rt : rterm t) :
   rpoly [seq (t * x)%T | x <- p] = rpoly p.
-Proof.
-by rewrite /rpoly all_map /= (@eq_all _ _ (@rterm _)) // => x; rewrite /= rt.
-Qed.
+Proof. by rewrite /rpoly all_map; apply/eq_all => x; rewrite /= rt. Qed.
 
 Lemma rmulpT (p q : polyF) : rpoly p -> rpoly q -> rpoly (mulpT p q).
 Proof.
@@ -242,7 +239,7 @@ Definition opppT : polyF -> polyF := map (GRing.Mul (- 1%T)%T).
 Lemma eval_opppT (p : polyF) (e : seq F) :
   eval_poly e (opppT p) = - eval_poly e p.
 Proof.
-by elim: p; rewrite /= ?oppr0 // => ? ? ->; rewrite !mulNr opprD polyC_opp mul1r.
+by elim: p; rewrite /= ?oppr0 // => ? ? ->; rewrite !mulNr opprD polyCN mul1r.
 Qed.
 
 Definition natmulpT n : polyF -> polyF := map (GRing.Mul n%:R%T).
@@ -251,7 +248,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 polyCMn; congr (_ + _).
 by rewrite -mulr_natl mulrAC -mulrA mulr_natl mulrC.
 Qed.
 
diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v
index 658258c..5359cce 100644
--- a/mathcomp/field/cyclotomic.v
+++ b/mathcomp/field/cyclotomic.v
@@ -50,10 +50,9 @@ End Ring.
 Lemma separable_Xn_sub_1 (R : idomainType) n :
   n%:R != 0 :> R -> @separable_poly R ('X^n - 1).
 Proof.
-case: n => [/eqP// | n nz_n]; rewrite /separable_poly linearB /=.
-rewrite derivC subr0 derivXn -scaler_nat coprimep_scaler //= exprS -scaleN1r.
-rewrite coprimep_sym coprimep_addl_mul coprimep_scaler ?coprimep1 //.
-by rewrite (signr_eq0 _ 1).
+case: n => [/eqP// | n nz_n]; rewrite /separable_poly linearB /= derivC subr0.
+rewrite derivXn -scaler_nat coprimepZr //= exprS -scaleN1r coprimep_sym.
+by rewrite coprimep_addl_mul coprimepZr ?coprimep1 // (signr_eq0 _ 1).
 Qed.
 
 Section Field.
@@ -188,7 +187,7 @@ have injf: injective (f e).
   rewrite modnMml -mulnA -modnMmr -{1}(mul1n e).
   by rewrite (chinese_modr co_e_n 0) modnMmr muln1 modn_small.
 rewrite [_ n](reindex_inj injf); apply: eq_big => k /=.
-  by rewrite coprime_modl coprime_mull co_e_n andbT.
+  by rewrite coprime_modl coprimeMl co_e_n andbT.
 by rewrite prim_expr_mod // mulnC exprM -Dz0.
 Qed.
 
@@ -269,7 +268,7 @@ have [|k_gt1] := leqP k 1; last have [p p_pr /dvdnP[k1 Dk]] := pdivP k_gt1.
   rewrite k0 /coprime gcd0n in cokn; rewrite (eqP cokn).
   rewrite -(size_map_inj_poly (can_inj intCK)) // -Df -Dpf.
   by rewrite -(subnKC g_gt1) -(subnKC (size_minCpoly z)) !addnS.
-move: cokn; rewrite Dk coprime_mull => /andP[cok1n].
+move: cokn; rewrite Dk coprimeMl => /andP[cok1n].
 rewrite prime_coprime // (dvdn_charf (char_Fp p_pr)) => /co_fg {co_fg}.
 have charFpX: p \in [char {poly 'F_p}].
   by rewrite (rmorph_char (polyC_rmorphism _)) ?char_Fp.
diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v
index bdff38a..db235fe 100644
--- a/mathcomp/field/falgebra.v
+++ b/mathcomp/field/falgebra.v
@@ -1173,11 +1173,11 @@ by rewrite -aimgM limgS // [rhs in (_ <= rhs)%VS]agenvEl addvSr.
 Qed.
 
 Lemma aimg_adjoin (f : ahom aT rT) U x : (f @: <<U; x>> = <<f @: U; f x>>)%VS.
-Proof. by rewrite aimg_agen limg_add limg_line. Qed.
+Proof. by rewrite aimg_agen limgD limg_line. Qed.
 
 Lemma aimg_adjoin_seq (f : ahom aT rT) U xs :
   (f @: <<U & xs>> = <<f @: U & map f xs>>)%VS.
-Proof. by rewrite aimg_agen limg_add limg_span. Qed.
+Proof. by rewrite aimg_agen limgD limg_span. Qed.
 
 Fact ker_sub_ahom_is_aspace (f g : ahom aT rT) :
   is_aspace (lker (ahval f - ahval g)).
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index df7ef5a..d99b69b 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -1290,8 +1290,8 @@ Qed.
 
 Fact mulfx_addl : left_distributive subfext_mul subfext_add.
 Proof.
-elim/quotW=> x; elim/quotW=> y; elim/quotW=> w; rewrite !piE /subfx_mul_rep.
-by rewrite linearD /= mulrDl modp_add linearD.
+elim/quotW=> x; elim/quotW=> y; elim/quotW=> w.
+by rewrite !piE /subfx_mul_rep linearD /= mulrDl modpD linearD.
 Qed.
 
 Fact nonzero1fx : subfext1 != subfext0.
@@ -1378,7 +1378,7 @@ Definition subfx_root := subfx_eval 'X.
 Lemma subfx_eval_is_rmorphism : rmorphism subfx_eval.
 Proof.
 do 2?split=> [x y|] /=; apply/eqP; rewrite piE.
-- by rewrite -linearB modp_add modNp.
+- by rewrite -linearB modpD modNp.
 - by rewrite /subfx_mul_rep !poly_rV_modp_K !(modp_mul, mulrC _ y).
 by rewrite modp_small // size_poly1 -subn_gt0 subn1.
 Qed.
@@ -1529,7 +1529,7 @@ suffices [L dimL [toPF [toL toPF_K toL_K]]]:
   elim/poly_ind: q => [|a q IHq].
     by rewrite map_poly0 horner0 linear0 mod0p.
   rewrite rmorphD rmorphM /= map_polyX map_polyC hornerMXaddC linearD /=.
-  rewrite linearZ /= -(rmorph1 toL) toL_K -modp_scalel alg_polyC modp_add.
+  rewrite linearZ /= -(rmorph1 toL) toL_K -modpZl alg_polyC modpD.
   congr (_ + _); rewrite -toL_K rmorphM /= -/z; congr (toPF (_ * z)).
   by apply: (can_inj toPF_K); rewrite toL_K.
 pose toL q : vL := poly_rV (q %% p); pose toPF (x : vL) := rVpoly x.
@@ -1547,13 +1547,13 @@ have mul1: left_id L1 mul.
   by move=> x; apply: toPinj; rewrite mulC !toL_K modp_mul mulr1 -toL_K toPF_K.
 have mulD: left_distributive mul +%R.
   move=> x y z; apply: toPinj; rewrite /toPF raddfD /= -!/(toPF _).
-  by rewrite !toL_K /toPF raddfD mulrDl modp_add.
+  by rewrite !toL_K /toPF raddfD mulrDl modpD.
 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 _).
-  by rewrite toL_K -scalerAl modp_scalel.
+  move=> a x y; apply: toPinj.
+  by rewrite toL_K /toPF !linearZ /= -!/(toPF _) toL_K -scalerAl modpZl.
 have mulZr: GRing.Algebra.axiom (LalgType F rL mulZl).
   by move=> a x y; rewrite !(mulrC x) scalerAl.
 pose aL := AlgType F _ mulZr; pose urL := FalgUnitRingType aL.
@@ -1567,7 +1567,7 @@ have unitE: GRing.Field.mixin_of urL.
     rewrite dvdp_gcdl -ltnNge /= => /eqp_size->.
     by rewrite (polySpred nz_p) ltnS size_poly.
   suffices: x * toL u.2 = 1 by exists (toL u.2); rewrite mulrC.
-  apply: toPinj; rewrite !toL_K -upq1 modp_mul modp_add mulrC.
+  apply: toPinj; rewrite !toL_K -upq1 modp_mul modpD mulrC.
   by rewrite modp_mull add0r.
 pose ucrL := [comUnitRingType of ComRingType urL mulC].
 have mul0 := GRing.Field.IdomainMixin unitE.
@@ -1575,8 +1575,7 @@ pose fL := FieldType (IdomainType ucrL mul0) unitE.
 exists [fieldExtType F of faL for fL]; first by rewrite dimvf; apply: mul1n.
 exists [linear of toPF as rVpoly].
 suffices toLM: lrmorphism (toL : {poly F} -> aL) by exists (LRMorphism toLM).
-have toLlin: linear toL.
-  by move=> a q1 q2; rewrite -linearP -modp_scalel -modp_add.
+have toLlin: linear toL by move=> a q1 q2; rewrite -linearP -modpZl -modpD.
 do ?split; try exact: toLlin; move=> q r /=.
 by apply: toPinj; rewrite !toL_K modp_mul -!(mulrC r) modp_mul.
 Qed.
@@ -1607,13 +1606,13 @@ have mul1: left_id L1 mul.
   by rewrite size_poly.
 have mulD: left_distributive mul +%R.
   move=> x y z; apply: canLR rVpolyK _.
-  by rewrite !raddfD mulrDl /= !toL_K /toL modp_add.
+  by rewrite !raddfD mulrDl /= !toL_K /toL modpD.
 have nzL1: L1 != 0 by rewrite -(can_eq rVpolyK) L1K 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: canRL rVpolyK _; rewrite !linearZ /= toL_K.
-  by rewrite -scalerAl modp_scalel.
+  move=> a x y; apply: canRL rVpolyK _.
+  by rewrite !linearZ /= toL_K -scalerAl modpZl.
 have mulZr: @GRing.Algebra.axiom _ (LalgType F rL mulZl).
   by move=> a x y; rewrite !(mulrC x) scalerAl.
 pose aL := AlgType F _ mulZr; pose urL := FalgUnitRingType aL.
@@ -1638,7 +1637,7 @@ have q_z q: rVpoly (map_poly iota q).[z] = q %% p.
   elim/poly_ind: q => [|a q IHq].
     by rewrite map_poly0 horner0 linear0 mod0p.
   rewrite rmorphD rmorphM /= map_polyX map_polyC hornerMXaddC linearD /=.
-  rewrite linearZ /= L1K alg_polyC modp_add; congr (_ + _); last first.
+  rewrite linearZ /= L1K alg_polyC modpD; congr (_ + _); last first.
     by rewrite modp_small // size_polyC; case: (~~ _) => //; apply: ltnW.
   by rewrite !toL_K IHq mulrC modp_mul mulrC modp_mul.
 exists z; first by rewrite /root -(can_eq rVpolyK) q_z modpp linear0.
diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v
index bc2eecb..e51a660 100644
--- a/mathcomp/field/separable.v
+++ b/mathcomp/field/separable.v
@@ -68,13 +68,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 /dvdpZr <-: 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[].
+  move: sep_p; rewrite coprimep_sym -[separable _](coprimepZl _ _ nz_c).
+  rewrite -(coprimepZr _ _ nz_c) -derivZ Dcp derivM coprimepMl.
+  by rewrite coprimep_addl_mul !coprimepMr -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.
@@ -82,9 +82,9 @@ have nz_g: g != 0.
 have [g_p]: g %| p /\ g %| p^`() by rewrite dvdp_gcdr ?dvdp_gcdl.
 pose c := lead_coef g ^+ scalp p g; have nz_c: c != 0 by rewrite lcn_neq0.
 have Dcp: c *: p = p %/ g * g by rewrite Pdiv.Idomain.divpK.
-rewrite nz_g andbT leqNgt -(dvdp_scaler _ _ nz_c) -derivZ Dcp derivM.
+rewrite nz_g andbT leqNgt -(dvdpZr _ _ nz_c) -derivZ Dcp derivM.
 rewrite dvdp_addr; last by rewrite dvdp_mull.
-rewrite Gauss_dvdpr; last by rewrite sq'p // mulrC -Dcp dvdp_scalel.
+rewrite Gauss_dvdpr; last by rewrite sq'p // mulrC -Dcp dvdpZl.
 by apply: contraL => /nz_der1p nz_g'; rewrite gtNdvdp ?nz_g' ?lt_size_deriv.
 Qed.
 
@@ -114,8 +114,8 @@ Proof.
 apply/idP/and3P => [sep_pq | [sep_p seq_q co_pq]].
   rewrite !(dvdp_separable _ sep_pq) ?dvdp_mulIr ?dvdp_mulIl //.
   by rewrite (separable_coprime sep_pq).
-rewrite /separable derivM coprimep_mull {1}addrC mulrC !coprimep_addl_mul.
-by rewrite !coprimep_mulr (coprimep_sym q p) co_pq !andbT; apply/andP.
+rewrite /separable derivM coprimepMl {1}addrC mulrC !coprimep_addl_mul.
+by rewrite !coprimepMr (coprimep_sym q p) co_pq !andbT; apply/andP.
 Qed.
 
 Lemma eqp_separable p q : p %= q -> separable p = separable q.
@@ -145,10 +145,10 @@ split=> [|u u_pg u_gt1]; last first.
   apply/eqP=> u'0 /=; have [k /negP[]] := max_dvd_u u u_gt1.
   elim: k => [|k IHk]; first by rewrite dvd1p.
   suffices: u ^+ k.+1 %| (p %/ g) * g.
-    by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdp_scaler ?lcn_neq0.
+    by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdpZr ?lcn_neq0.
   rewrite exprS dvdp_mul // dvdp_gcd IHk //=.
   suffices: u ^+ k %| (p %/ u ^+ k * u ^+ k)^`().
-    by rewrite Pdiv.Idomain.divpK // derivZ dvdp_scaler ?lcn_neq0.
+    by rewrite Pdiv.Idomain.divpK // derivZ dvdpZr ?lcn_neq0.
   by rewrite !derivCE u'0 mul0r mul0rn mulr0 addr0 dvdp_mull.
 have pg_dv_p: p %/ g %| p by rewrite divp_dvd ?dvdp_gcdl.
 apply/poly_square_freeP=> u; rewrite neq_ltn ltnS leqn0 size_poly_eq0.
@@ -157,11 +157,11 @@ case/predU1P=> [-> | /max_dvd_u[k]].
 apply: contra => u2_dv_pg; case: k; [by rewrite dvd1p | elim=> [|n IHn]].
   exact: dvdp_trans (dvdp_mulr _ _) (dvdp_trans u2_dv_pg pg_dv_p).
 suff: u ^+ n.+2 %| (p %/ g) * g.
-  by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdp_scaler ?lcn_neq0.
+  by rewrite Pdiv.Idomain.divpK ?dvdp_gcdl // dvdpZr ?lcn_neq0.
 rewrite -add2n exprD dvdp_mul // dvdp_gcd.
 rewrite (dvdp_trans _ IHn) ?exprS ?dvdp_mull //=.
 suff: u ^+ n %| ((p %/ u ^+ n.+1) * u ^+ n.+1)^`().
-  by rewrite Pdiv.Idomain.divpK // derivZ dvdp_scaler ?lcn_neq0.
+  by rewrite Pdiv.Idomain.divpK // derivZ dvdpZr ?lcn_neq0.
 by rewrite !derivCE dvdp_add // -1?mulr_natl ?exprS !dvdp_mull.
 Qed.
 
@@ -260,7 +260,7 @@ without loss{nz_q} sep_q: q qy_0 / separable_poly q.
   rewrite Dq rmorphM /= gcdp_map -(eqp_dvdr _ (gcdp_mul2l _ _ _)) -deriv_map Dr.
   rewrite dvdp_gcd derivM deriv_exp derivXsubC mul1r !mulrA dvdp_mulIr /=.
   rewrite mulrDr mulrA dvdp_addr ?dvdp_mulIr // exprS -scaler_nat -!scalerAr.
-  rewrite dvdp_scaler -?(rmorph_nat iota) ?fmorph_eq0 ?charF0 //.
+  rewrite dvdpZr -?(rmorph_nat iota) ?fmorph_eq0 ?charF0 //.
   rewrite mulrA dvdp_mul2r ?expf_neq0 ?polyXsubC_eq0 //.
   by rewrite Gauss_dvdpl ?dvdp_XsubCl // coprimep_sym coprimep_XsubC.
 have [r nz_r PETxy] := large_field_PET qy_0 sep_q.
@@ -585,7 +585,7 @@ elim: n => // n IHn in x @d *; rewrite ltnS => le_d_n.
 have [[p charLp]|] := altP (separablePn K x); last by rewrite negbK; exists 1%N.
 case=> g Kg defKx; have p_pr := charf_prime charLp.
 suffices /IHn[m /andP[charLm sepKxpm]]: adjoin_degree K (x ^+ p) < n.
-  by exists (p * m)%N; rewrite pnat_mul pnatE // charLp charLm exprM.
+  by exists (p * m)%N; rewrite pnatM pnatE // charLp charLm exprM.
 apply: leq_trans le_d_n; rewrite -ltnS -!size_minPoly.
 have nzKx: minPoly K x != 0 by rewrite monic_neq0 ?monic_minPoly.
 have nzg: g != 0 by apply: contra_eqN defKx => /eqP->; rewrite comp_poly0.
@@ -844,7 +844,7 @@ Lemma inseparable_add K x y :
 Proof.
 have insepP := purely_inseparable_elementP.
 move=> /insepP[n charLn Kxn] /insepP[m charLm Kym]; apply/insepP.
-have charLnm: [char L].-nat (n * m)%N by rewrite pnat_mul charLn.
+have charLnm: [char L].-nat (n * m)%N by rewrite pnatM charLn.
 by exists (n * m)%N; rewrite ?exprDn_char // {2}mulnC !exprM memvD // rpredX.
 Qed.
 
@@ -944,7 +944,7 @@ by apply/FadjoinP/andP; rewrite sKE separable_generator_mem.
 Qed.
 
 Lemma separable_refl K : separable K K.
-Proof. by apply/separableP; apply: base_separable. Qed.
+Proof. exact/separableP/base_separable. Qed.
 
 Lemma separable_trans M K E : separable K M -> separable M E -> separable K E.
 Proof.
@@ -986,7 +986,7 @@ Proof.
 have insepP := purely_inseparableP => /insepP insepK_M /insepP insepM_E.
 have insepPe := purely_inseparable_elementP.
 apply/insepP=> x /insepM_E/insepPe[n charLn /insepK_M/insepPe[m charLm Kxnm]].
-by apply/insepPe; exists (n * m)%N; rewrite ?exprM // pnat_mul charLn charLm.
+by apply/insepPe; exists (n * m)%N; rewrite ?exprM // pnatM charLn charLm.
 Qed.
 
 End Separable.