Switch from long suffixes to short suffixes

8 files changed, 36 insertions, 38 deletions

diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 469c649..ba26ab6 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -177,7 +177,7 @@ have [-> | nt_x] := eqVneq x 1.
 apply: (iffP idP) => [/eqP | [p p_pr /eqP x_pn]].
   by exists (pdiv #[x]); rewrite ?pdiv_prime ?order_gt1.
 rewrite (@pdiv_p_elt p) //; rewrite -order_dvdn in x_pn.
-by rewrite [p_elt _ _](pnat_dvd x_pn) // pnat_exp pnat_id.
+by rewrite [p_elt _ _](pnat_dvd x_pn) // pnatX pnat_id.
 Qed.
 
 Lemma Mho_p_elt (p : nat) x : x \in A -> p.-elt x -> x ^+ (p ^ n) \in Mho.
@@ -390,7 +390,7 @@ Proof. by rewrite /abelem pgroup1 abelian1 exponent1 dvd1n. Qed.
 Lemma abelemE p G : prime p -> p.-abelem G = abelian G && (exponent G %| p).
 Proof.
 move=> p_pr; rewrite /abelem -pnat_exponent andbA -!(andbC (_ %| _)).
-by case: (dvdn_pfactor _ 1 p_pr) => // [[k _ ->]]; rewrite pnat_exp pnat_id.
+by case: (dvdn_pfactor _ 1 p_pr) => // [[k _ ->]]; rewrite pnatX pnat_id.
 Qed.
 
 Lemma abelemP p G :
@@ -2177,4 +2177,3 @@ Lemma fin_ring_char_abelem p (R : finRingType) :
 Proof. exact: fin_lmod_char_abelem [finLmodType R of R^o]. Qed.
 
 End FimModAbelem.
-
diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v
index 58c3cf0..2dcb1d5 100644
--- a/mathcomp/solvable/extraspecial.v
+++ b/mathcomp/solvable/extraspecial.v
@@ -182,7 +182,7 @@ by exists 1%R; rewrite ?inE.
 Qed.
 
 Lemma pX1p2_pgroup : p.-group p^{1+2}.
-Proof. by rewrite /pgroup card_pX1p2 pnat_exp pnat_id. Qed.
+Proof. by rewrite /pgroup card_pX1p2 pnatX pnat_id. Qed.
 
 (* This is part of the existence half of Aschbacher ex. (8.7)(1) *)
 Lemma pX1p2_extraspecial : extraspecial p^{1+2}.
@@ -207,7 +207,7 @@ have ->: p^{1+2} = 'Ohm_1(p^{1+2}).
   case/existsP: (isoGrp_hom Grp_pX1p2) => [[x y]] /=.
   case/eqP=> <- xp yp _ _; rewrite joing_idl joing_idr genS //.
   by rewrite subsetI subset_gen subUset !sub1set !inE xp yp!eqxx.
-rewrite exponent_Ohm1_class2 ?card_pX1p2 ?odd_exp // nil_class2.
+rewrite exponent_Ohm1_class2 ?card_pX1p2 ?oddX // nil_class2.
 by have [[_ ->] _ ] := pX1p2_extraspecial.
 Qed.
 
@@ -217,7 +217,7 @@ Lemma isog_pX1p2 (gT : finGroupType) (G : {group gT}) :
 Proof.
 move=> esG expGp oG; apply/(isoGrpP _ Grp_pX1p2).
 rewrite card_pX1p2; split=> //.
-have pG: p.-group G by rewrite /pgroup oG pnat_exp pnat_id.
+have pG: p.-group G by rewrite /pgroup oG pnatX pnat_id.
 have oZ := card_center_extraspecial pG esG.
 have [x Gx notZx]: exists2 x, x \in G & x \notin 'Z(G).
   apply/subsetPn; rewrite proper_subn // properEcard center_sub oZ oG.
@@ -283,7 +283,7 @@ by rewrite oG oZ IHn -expnD mulKn ?prime_gt0.
 Qed.
 
 Lemma pX1p2n_pgroup n : prime p -> p.-group p^{1+2*n}.
-Proof. by move=> p_pr; rewrite /pgroup card_pX1p2n // pnat_exp pnat_id. Qed.
+Proof. by move=> p_pr; rewrite /pgroup card_pX1p2n // pnatX pnat_id. Qed.
 
 (* This is part of the existence half of Aschbacher (23.13) *)
 Lemma exponent_pX1p2n n : prime p -> odd p -> exponent p^{1+2*n} = p.
@@ -526,7 +526,7 @@ Lemma isog_pX1p2n n (gT : finGroupType) (G : {group gT}) :
 Proof.
 move=> p_pr esG oG expG; have p_gt1 := prime_gt1 p_pr.
 have not_le_p3_p: ~~ (p ^ 3 <= p) by rewrite (leq_exp2l 3 1).
-have pG: p.-group G by rewrite /pgroup oG pnat_exp pnat_id.
+have pG: p.-group G by rewrite /pgroup oG pnatX pnat_id.
 have oZ := card_center_extraspecial pG esG.
 have{pG esG} [Es p3Es defG] := extraspecial_structure pG esG.
 set Z := 'Z(G) in oZ defG p3Es.
@@ -614,7 +614,7 @@ by rewrite -muln_divA // mulnC -(expnD 2 2).
 Qed.
 
 Lemma DnQ_pgroup n : 2.-group 'D^n*Q.
-Proof. by rewrite /pgroup card_DnQ pnat_exp. Qed.
+Proof. by rewrite /pgroup card_DnQ pnatX. Qed.
 
 (* Final part of the existence half of Aschbacher (23.14). *)
 Lemma DnQ_extraspecial n : extraspecial 'D^n*Q.
@@ -659,7 +659,7 @@ Proof.
 elim: n G => [|n IHn] G oG esG.
   case/negP: (extraspecial_nonabelian esG).
   by rewrite cyclic_abelian ?prime_cyclic ?oG.
-have pG: 2.-group G by rewrite /pgroup oG pnat_exp.
+have pG: 2.-group G by rewrite /pgroup oG pnatX.
 have oZ:= card_center_extraspecial pG esG.
 have: 'Z(G) \subset 'Ohm_1(G).
   apply/subsetP=> z Zz; rewrite (OhmE _ pG) mem_gen //.
@@ -705,7 +705,7 @@ have AutZin2_1p2: Aut_in (Aut 2^{1+2}) 'Z(2^{1+2}) \isog Aut 'Z(2^{1+2}).
 have [isoR | isoR] := IHn R oR esR.
   by left; case: pX1p2S => gz isoZ; rewrite (isog_cprod_by _ defG).
 have n_gt0: n > 0.
-  have pR: 2.-group R by rewrite /pgroup oR pnat_exp.
+  have pR: 2.-group R by rewrite /pgroup oR pnatX.
   have:= min_card_extraspecial pR esR.
   by rewrite oR leq_exp2l // ltnS (leq_double 1).
 case: DnQ_P isoR => gR isoZR /=; rewrite isog_sym; case/isogP=> fR injfR im_fR.
@@ -742,7 +742,7 @@ elim: n => [|n IHn]; first by rewrite p_rank_abelem ?prime_abelem ?card_pX1p2n.
 have oDDn: #|'D^n.+1| = (2 ^ n.+1.*2.+1)%N by apply: card_pX1p2n.
 have esDDn: extraspecial 'D^n.+1 by apply: pX1p2n_extraspecial.
 do [case: pX1p2S => gz isoZ; set DDn := [set: _]] in oDDn esDDn *.
-have pDDn: 2.-group DDn by rewrite /pgroup oDDn pnat_exp.
+have pDDn: 2.-group DDn by rewrite /pgroup oDDn pnatX.
 apply/eqP; rewrite eqn_leq; apply/andP; split.
   have [E EprE]:= p_rank_witness 2 [group of DDn].
   have [sEDDn abelE <-] := pnElemP EprE; have [pE cEE _]:= and3P abelE.
diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v
index 8185773..a0c40ee 100644
--- a/mathcomp/solvable/extremal.v
+++ b/mathcomp/solvable/extremal.v
@@ -350,7 +350,7 @@ have os: #[s] = (p ^ (n - e0))%N.
   case/dvdn_pfactor=> // d; rewrite leq_eqVlt.
   case/predU1P=> [-> // | lt_d os]; case/idPn: (p_gt1); rewrite -os0.
   by rewrite order_gt1 negbK -order_dvdn os dvdn_exp2l // -ltnS -subSn.
-have p_s: p.-elt s by rewrite /p_elt os pnat_exp ?pnat_id.
+have p_s: p.-elt s by rewrite /p_elt os pnatX ?pnat_id.
 have defS1: 'Ohm_1(<[s]>) = <[s0]>.
   apply/eqP; rewrite eq_sym eqEcard cycle_subG -orderE os0.
   rewrite (Ohm1_cyclic_pgroup_prime _ p_s) ?cycle_cyclic ?leqnn ?cycle_eq1 //=.
@@ -398,7 +398,7 @@ Lemma extremal_generators_facts gT (G : {group gT}) p n x y :
       <[x]> * <[y]> = G & <[y]> \subset 'N(<[x]>)].
 Proof.
 move=> p_pr [oG Gx ox] /setDP[Gy notXy].
-have pG: p.-group G by rewrite /pgroup oG pnat_exp pnat_id.
+have pG: p.-group G by rewrite /pgroup oG pnatX pnat_id.
 have maxX: maximal <[x]> G.
   rewrite p_index_maximal -?divgS ?cycle_subG // -orderE oG ox.
   case: (n) oG => [|n' _]; last by rewrite -expnB ?subSnn ?leqnSn ?prime_gt0.
@@ -438,7 +438,7 @@ rewrite /modular_gtype def_p def_q def_r; apply: Extremal.Grp => //.
 set B := <[_]>; have Bb: Zp1 \in B by apply: cycle_id.
 have oB: #|B| = q by rewrite -orderE order_Zp1 Zp_cast.
 have cycB: cyclic B by rewrite cycle_cyclic.
-have pB: p.-group B by rewrite /pgroup oB pnat_exp ?pnat_id.
+have pB: p.-group B by rewrite /pgroup oB pnatX ?pnat_id.
 have ntB: B != 1 by rewrite -cardG_gt1 oB.
 have [] := cyclic_pgroup_Aut_structure pB cycB ntB.
 rewrite oB pfactorK //= -/B -(expg_znat r.+1 Bb) oB => mB [[def_mB _ _ _ _] _].
@@ -711,7 +711,7 @@ rewrite !expnS !mulKn // -!expnS /=; set q := (2 ^ _)%N.
 have q_gt1: q > 1 by rewrite (ltn_exp2l 0).
 apply: Extremal.Grp => //; set B := <[_]>.
 have oB: #|B| = q by rewrite -orderE order_Zp1 Zp_cast.
-have pB: 2.-group B by rewrite /pgroup oB pnat_exp.
+have pB: 2.-group B by rewrite /pgroup oB pnatX.
 have ntB: B != 1 by rewrite -cardG_gt1 oB.
 have [] := cyclic_pgroup_Aut_structure pB (cycle_cyclic _) ntB.
 rewrite oB /= pfactorK //= -/B => m [[def_m _ _ _ _] _].
@@ -1133,7 +1133,7 @@ have def_ur: {in G, forall t, #[t] = 2 -> t = u ^+ r}.
   move=> t Gt /= ot; case Ut: (t \in <[u]>); last first.
     move/eqP: ot; rewrite eqn_dvd order_dvdn -order_eq1 U'2 ?our //.
     by rewrite defUv inE Ut.
-  have p2u: 2.-elt u by rewrite /p_elt ou pnat_exp.
+  have p2u: 2.-elt u by rewrite /p_elt ou pnatX.
   have: t \in 'Ohm_1(<[u]>).
     by rewrite (OhmE _ p2u) mem_gen // !inE Ut -order_dvdn ot.
   rewrite (Ohm_p_cycle _ p2u) ou pfactorK // subn1 -/r cycle_traject our !inE.
@@ -1338,7 +1338,7 @@ have xy2: (x * y) ^+ 2 = x ^+ r.
 have oxy: #[x * y] = 4 by rewrite (@orderXprime _ 2 2) ?xy2.
 have r_gt2: r > 2 by rewrite (ltn_exp2l 1) // -(subnKC n_gt3).
 have coXr1: coprime #[x] (2 ^ (n - 3)).-1.
-  rewrite ox coprime_expl // -(@coprime_pexpl (n - 3)) ?coprimenP ?subn_gt0 //.
+  rewrite ox coprimeXl // -(@coprime_pexpl (n - 3)) ?coprimenP ?subn_gt0 //.
   by rewrite expn_gt0.
 have def2r1: (2 * (2 ^ (n - 3)).-1).+1 = r.-1.
   rewrite -!subn1 mulnBr -expnS [_.+1]subnSK ?(ltn_exp2l 0) //.
@@ -1584,11 +1584,11 @@ Lemma odd_not_extremal2 : odd #|G| -> ~~ extremal2 G.
 Proof.
 rewrite /extremal2 /extremal_class; case: logn => // n'.
 case: andP => [[n_gt1 isoG] | _].
-  by rewrite (card_isog isoG) card_2dihedral ?odd_exp.
+  by rewrite (card_isog isoG) card_2dihedral ?oddX.
 case: andP => [[n_gt2 isoG] | _].
-  by rewrite (card_isog isoG) card_quaternion ?odd_exp.
+  by rewrite (card_isog isoG) card_quaternion ?oddX.
 case: andP => [[n_gt3 isoG] | _].
-  by rewrite (card_isog isoG) card_semidihedral ?odd_exp.
+  by rewrite (card_isog isoG) card_semidihedral ?oddX.
 by case: ifP.
 Qed.
 
@@ -1784,7 +1784,7 @@ have[i def_yp]: exists i, y ^- p = x ^+ i.
 have p_i: p %| i.
   apply: contraR notXy; rewrite -prime_coprime // => co_p_j.
   have genX: generator X (y ^- p).
-    by rewrite def_yp defX generator_coprime ox coprime_expl.
+    by rewrite def_yp defX generator_coprime ox coprimeXl.
   rewrite -scXG (setIidPl _) // centsC ((X :=P: _) genX) cycle_subG groupV.
   rewrite /= -(defG 0%N) mul1g centY inE -defX (subsetP cXX) ?X_Gp //.
   by rewrite (subsetP (cycle_abelian y)) ?mem_cycle.
@@ -1877,7 +1877,7 @@ have modM1 (M : {group gT}):
   have n_gt2: n > 2 by apply: leq_trans (leq_addl _ _) n_gt23.
   have def_n: n = (n - 3).+3 by rewrite -{1}(subnKC n_gt2).
   have oM: #|M| = (q ^ n)%N by rewrite (card_isog isoM) card_modular_group.
-  have pM: q.-group M by rewrite /pgroup oM pnat_exp pnat_id.
+  have pM: q.-group M by rewrite /pgroup oM pnatX pnat_id.
   have def_q: q = p; last rewrite {q q_pr}def_q in oM pM isoM n_gt23.
     by apply/eqP; rewrite eq_sym [p == q](pgroupP pM) // -iUM dvdn_indexg.
   have [[x y] genM modM] := generators_modular_group p_pr n_gt2 isoM.
diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v
index a96295f..73188a6 100644
--- a/mathcomp/solvable/gseries.v
+++ b/mathcomp/solvable/gseries.v
@@ -132,7 +132,7 @@ have:= sKG; rewrite subEproper => /predU1P[<-|prKG]; first exact: IHm.
 pose L := [group of f G].
 have sHK: H \subset K by case/IHm: Hsn.
 have sLK: L \subset K by rewrite gen_subG class_support_sub_norm.
-rewrite -(subnK (proper_card (sub_proper_trans sLK prKG))) iter_add iterSr.
+rewrite -(subnK (proper_card (sub_proper_trans sLK prKG))) iterD iterSr.
 have defH: H = setIgr L H by rewrite -sub_setIgr ?sub_gen ?sub_class_support.
 have: normal.-series H (map (setIgr L) s) by rewrite defH path_setIgr.
 case/IHm=> [|_]; first by rewrite size_map.
diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v
index 119a9fc..6bd5e0d 100644
--- a/mathcomp/solvable/hall.v
+++ b/mathcomp/solvable/hall.v
@@ -117,7 +117,7 @@ have [sMG nMG] := andP nsMG; rewrite -defG => sK1G coHK oK1K.
 have nMsG (L : {set gT}): L \subset G -> L \subset 'N(M).
   by move/subset_trans->.
 have [coKM coHMK]: coprime #|M| #|K| /\ coprime #|H / M| #|K|.
-  by apply/andP; rewrite -coprime_mull card_quotient ?nMsG ?Lagrange.
+  by apply/andP; rewrite -coprimeMl card_quotient ?nMsG ?Lagrange.
 have oKM (K' : {group gT}): K' \subset G -> #|K'| = #|K| -> #|K' / M| = #|K|.
   move=> sK'G oK'.
   rewrite -quotientMidr -?norm_joinEl ?card_quotient ?nMsG //; last first.
@@ -248,7 +248,7 @@ have{pi'Hb'} pi'H': pi^'.-nat #|G : H|.
   by rewrite -(divnMl (cardG_gt0 M)) !Lagrange.
 have [pi_p | pi'p] := boolP (p \in pi).
   exists H => //; apply/and3P; split=> //; rewrite /pgroup.
-  by rewrite -(Lagrange sMH) -card_quotient // pnat_mul -def_H (pi_pnat pM).
+  by rewrite -(Lagrange sMH) -card_quotient // pnatM -def_H (pi_pnat pM).
 have [ltHG | leGH {n IHn leGn transH}] := ltnP #|H| #|G|.
   case: (IHn _ H (leq_trans ltHG leGn)) => [|H1]; first exact: solvableS solG.
   case/and3P=> sH1H piH1 pi'H1' transH1.
@@ -256,7 +256,7 @@ have [ltHG | leGH {n IHn leGn transH}] := ltnP #|H| #|G|.
   exists H1 => [|K sKG piK].
     apply/and3P; split => //.
     rewrite -divgS // -(Lagrange sHG) -(Lagrange sH1H) -mulnA.
-    by rewrite mulKn // pnat_mul pi'H1'.
+    by rewrite mulKn // pnatM pi'H1'.
   case: (transH K sKG piK) => x Gx def_K.
   case: (transH1 (K :^ x^-1)%G) => [||y Hy def_K1].
   - by rewrite sub_conjgV.
@@ -608,7 +608,7 @@ have{nHAq} nHMA: A \subset 'N(HM).
   by rewrite -(quotientSGK nMA) ?normsG ?quotient_normG -?defHM //; apply/andP.
 case/orP: (orbN (p \in pi)) => pi_p.
   exists HM; split=> //; apply/and3P; split; rewrite /pgroup //.
-  by rewrite -(Lagrange sMHM) pnat_mul -card_quotient // -defHM (pi_pnat pM).
+  by rewrite -(Lagrange sMHM) pnatM -card_quotient // -defHM (pi_pnat pM).
 case: (ltnP #|HM| #|G|) => [ltHG | leGHM {n IHn leGn}].
   case: (IHn _ A HM X (leq_trans ltHG leGn)) => // [||H [hallH nHA sXH]].
   - exact: coprimeSg coGA.
@@ -617,7 +617,7 @@ case: (ltnP #|HM| #|G|) => [ltHG | leGHM {n IHn leGn}].
   have sHG: H \subset G by apply: subset_trans sHMG.
   exists H; split=> //; apply/and3P; split=> //.
   rewrite -divgS // -(Lagrange sHMG) -(Lagrange sHHM) -mulnA mulKn //.
-  by rewrite pnat_mul pi'H'.
+  by rewrite pnatM pi'H'.
 have{leGHM nHMA sHMG sMHM sXHM pi'HM'} eqHMG: HM = G.
   by apply/eqP; rewrite -val_eqE eqEcard sHMG.
 have pi'M: pi^'.-group M by rewrite /pgroup (pi_pnat pM).
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index 3786cff..af0001c 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -834,7 +834,7 @@ Lemma card_p3group_extraspecial E :
   prime p -> #|E| = (p ^ 3)%N -> #|'Z(E)| = p -> extraspecial E.
 Proof.
 move=> p_pr oEp3 oZp; have p_gt0 := prime_gt0 p_pr.
-have pE: p.-group E by rewrite /pgroup oEp3 pnat_exp pnat_id.
+have pE: p.-group E by rewrite /pgroup oEp3 pnatX pnat_id.
 have pEq: p.-group (E / 'Z(E))%g by rewrite quotient_pgroup.
 have /andP[sZE nZE] := center_normal E.
 have oEq: #|E / 'Z(E)|%g = (p ^ 2)%N.
@@ -1248,7 +1248,7 @@ have [p2 | odd_p] := even_prime p_pr.
   suffices <-: restr_perm 'Z(E) @* Aut E = Aut 'Z(E) by apply: Aut_in_isog.
   apply/eqP; rewrite eqEcard restr_perm_Aut ?center_sub //=.
   by rewrite card_Aut_cyclic ?prime_cyclic ?oZE // {1}p2 cardG_gt0.
-have pE: p.-group E by rewrite /pgroup oE pnat_exp pnat_id.
+have pE: p.-group E by rewrite /pgroup oE pnatX pnat_id.
 have nZE: E \subset 'N('Z(E)) by rewrite normal_norm ?center_normal.
 have esE: extraspecial E := card_p3group_extraspecial p_pr oE oZE.
 have [[defPhiE defE'] prZ] := esE.
@@ -1303,7 +1303,7 @@ pose f := Morphism fM; have fK: f @* K = K.
   apply/setP=> u; rewrite morphimEdom.
   apply/imsetP/idP=> [[v Kv ->] | Ku]; first exact: groupX.
   exists (u ^+ expg_invn K (val k)); first exact: groupX.
-  rewrite /f /= expgAC expgK // oK coprime_expl // -unitZpE //.
+  rewrite /f /= expgAC expgK // oK coprimeXl // -unitZpE //.
   by case: (k) => /=; rewrite orderE -defZ oZE => j; rewrite natr_Zp.
 have fMact: {in K & <[x]>, morph_act 'J 'J f (idm <[x]>)}.
   by move=> u v _ _; rewrite /= conjXg.
diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v
index 2ed68f0..c9ce3b0 100644
--- a/mathcomp/solvable/pgroup.v
+++ b/mathcomp/solvable/pgroup.v
@@ -198,7 +198,7 @@ Lemma pgroupM pi G H : pi.-group (G * H) = pi.-group G && pi.-group H.
 Proof.
 have GH_gt0: 0 < #|G :&: H| := cardG_gt0 _.
 rewrite /pgroup -(mulnK #|_| GH_gt0) -mul_cardG -(LagrangeI G H) -mulnA.
-by rewrite mulKn // -(LagrangeI H G) setIC !pnat_mul andbCA; case: (pnat _).
+by rewrite mulKn // -(LagrangeI H G) setIC !pnatM andbCA; case: (pnat _).
 Qed.
 
 Lemma pgroupJ pi G x : pi.-group (G :^ x) = pi.-group G.
@@ -548,8 +548,7 @@ Proof.
 move=> pi12; rewrite -{2}(consttC pi2 x) consttM; last exact: commuteX2.
 rewrite (constt1P _ x.`_pi2^' _) ?mulg1 //.
 apply: sub_in_pnat (p_elt_constt _ x) => p; rewrite order_constt => pi_p.
-apply: contra; apply: pi12.
-by rewrite -[#[x]](partnC pi2^') // primes_mul // pi_p.
+by apply/contra/pi12; rewrite -[#[x]](partnC pi2^') // primesM // pi_p.
 Qed.
 
 Lemma prod_constt x : \prod_(0 <= p < #[x].+1) x.`_p = x.
@@ -693,7 +692,7 @@ case/Cauchy=> //= Hx; rewrite -sub1set -gen_subG -/<[Hx]> /order.
 case/inv_quotientS=> //= K -> sHK sKG {Hx}.
 rewrite card_quotient ?(subset_trans sKG) // => iKH; apply/negP=> pi_p.
 rewrite -iKH -divgS // (maxH K) ?divnn ?cardG_gt0 // in p_pr.
-by rewrite /psubgroup sKG /pgroup -(Lagrange sHK) mulnC pnat_mul iKH pi_p.
+by rewrite /psubgroup sKG /pgroup -(Lagrange sHK) mulnC pnatM iKH pi_p.
 Qed.
 
 Lemma setI_normal_Hall G H K :
@@ -725,7 +724,7 @@ Lemma pmorphim_pgroup pi G :
 Proof.
 move=> piker sGD; apply/idP/idP=> [pifG|]; last exact: morphim_pgroup.
 apply: (@pgroupS _ _ (f @*^-1 (f @* G))); first by rewrite -sub_morphim_pre.
-by rewrite /pgroup card_morphpre ?morphimS // pnat_mul; apply/andP.
+by rewrite /pgroup card_morphpre ?morphimS // pnatM; apply/andP.
 Qed.
 
 Lemma morphim_p_index pi G H :
diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v
index aed6351..fcbe7e8 100644
--- a/mathcomp/solvable/sylow.v
+++ b/mathcomp/solvable/sylow.v
@@ -267,7 +267,7 @@ Qed.
 
 Lemma card_p2group_abelian P : prime p -> #|P| = (p ^ 2)%N -> abelian P.
 Proof.
-move=> primep oP; have pP: p.-group P by rewrite /pgroup oP pnat_exp pnat_id.
+move=> primep oP; have pP: p.-group P by rewrite /pgroup oP pnatX pnat_id.
 by rewrite (p2group_abelian pP) // oP pfactorK.
 Qed.