diff --git a/theories/BGsection12.v b/theories/BGsection12.v
index 440771a..ef0d728 100644
--- a/theories/BGsection12.v
+++ b/theories/BGsection12.v
@@ -306,7 +306,7 @@ have SylowE3 P: Sylow E3 P -> [/\ cyclic P, P \subset E^`(1) & 'C_P(E) = 1].
     have sP_Ep'P: P \subset 'O_p^'(E) <*> P := joing_subr _ _.
     have sylP_Ep'P := pHall_subl sP_Ep'P (normal_sub nsEp'P_E) sylP_E.
     rewrite -{2}(Frattini_arg nsEp'P_E sylP_Ep'P) /= !norm_joinEr //.
-    by rewrite -mulgA (normC nPK) -mulPK -{1}(mulGid P) !mulgA.
+    by rewrite -[LHS]mulgA (normC nPK) -mulPK -{1}(mulGid P) !mulgA.
   have ntPE': P :&: E^`(1) != 1.
     have sylPE' := Hall_setI_normal (der_normal 1 E) sylP_E.
     rewrite -rank_gt0 (rank_Sylow sylPE') p_rank_gt0.
diff --git a/theories/BGsection16.v b/theories/BGsection16.v
index a29b2ca..83287e9 100644
--- a/theories/BGsection16.v
+++ b/theories/BGsection16.v
@@ -411,7 +411,7 @@ rewrite /FTtype (eq_p'group _ (kappaJ _ _)) pgroupJ MsigmaJ FcoreJ derJ.
 rewrite !(can_eq (conjsgK x)); do 4!congr (if _ then _ else _).
 rewrite -quotientInorm normJ -conjIg /= setIC -{1 3}(setIidPr (normG M`_\F)).
 rewrite -!morphim_conj -morphim_quotm ?normalG //= => nsMFN.
-by rewrite injm_abelian /= ?im_quotient // injm_quotm ?injm_conj.
+by rewrite injm_abelian/= ?im_quotient?/reverse_coercion ?injm_quotm ?injm_conj.
 Qed.
 
 Lemma FTcoreJ M x : (M :^ x)`_\s = M`_\s :^ x.
diff --git a/theories/BGsection2.v b/theories/BGsection2.v
index ace2586..f59dcd4 100644
--- a/theories/BGsection2.v
+++ b/theories/BGsection2.v
@@ -1138,7 +1138,7 @@ split.
   have Ur: r \in GRing.unit.
     by rewrite -(unitrX_pos _ (prime_gt0 q_pr)) rq1 unitr1.
   pose u_r : {unit 'F_p} := Sub r Ur; have:= order_dvdG (in_setT u_r).
-  rewrite card_units_Zp ?pdiv_gt0 // {2}/pdiv primes_prime //=.
+  rewrite card_units_Zp ?pdiv_gt0 // [X in totient X]/pdiv primes_prime //=.
   rewrite (@totient_pfactor p 1) // muln1; apply: dvdn_trans.
   have: (u_r ^+ q == 1)%g.
     by rewrite -val_eqE unit_Zp_expg -Zp_nat natrX natr_Zp rq1.
diff --git a/theories/BGsection3.v b/theories/BGsection3.v
index 99f33be..b78b328 100644
--- a/theories/BGsection3.v
+++ b/theories/BGsection3.v
@@ -548,7 +548,7 @@ have irrK'K: mx_absolutely_irreducible rK'K.
       by rewrite mem_enum.
     by rewrite PackSocleK.
   have [i def_i]: exists i, [set: sK'G'] = [set i].
-    apply/cards1P; rewrite -dvdn1 -{7}(eqnP coKp) dvdn_gcd.
+  apply/cards1P; rewrite -dvdn1 -[X in _ %| X](eqnP coKp) dvdn_gcd.
     by rewrite -{1}eq_sK' sK'_dv_K sK'_dv_p.
   pose M := socle_base i; have simM : mxsimple rK'G' M := socle_simple i.
   have cycGq: cyclic (G' / K^`(1)).
diff --git a/theories/PFsection9.v b/theories/PFsection9.v
index 32ff619..33fe14b 100644
--- a/theories/PFsection9.v
+++ b/theories/PFsection9.v
@@ -411,7 +411,8 @@ pose phi w := invm (inj_Zp_h w) \o restr_perm <[h ^ w]> \o actperm 'Q.
 have dU w: w \in W1bar -> {subset U <= 'dom (phi w)}.
   move=> Ww x Ux; have Qx := subsetP (acts_dom actsUH1) x Ux.
   rewrite inE Qx /= im_Zp_unitm inE mem_morphpre //=; last first.
-    by apply: Aut_restr_perm (actperm_Aut 'Q _); rewrite //= quotientT.
+    by apply: Aut_restr_perm (actperm_Aut 'Q _);
+      rewrite //= quotientT?/reverse_coercion.
   rewrite cycleJ -defH1 !inE /=; apply/subsetP=> z H1w_z; rewrite inE actpermK.
   rewrite qactJ (subsetP nH0U) ?memJ_norm // normJ mem_conjg.
   by rewrite (subsetP nH1U) // -mem_conjg (normsP nUW1b) ?mem_quotient.
@@ -531,8 +532,8 @@ have cEE A: A \in E_U -> centgmx rU A.
   apply/row_matrixP=> i; rewrite row_mul; move: (row i _) => h.
   have cHbH': (U / H0)^`(1) \subset 'C(Hbar).
     by rewrite -quotient_der ?quotient_cents.
-  apply: rVabelem_inj; rewrite rVabelemJ ?groupR //.
-  by apply: (canLR (mulKg _)); rewrite -(centsP cHbH') ?mem_commg ?mem_rVabelem.
+  apply: rVabelem_inj; rewrite rVabelemJ ?groupR //; apply: (canLR (mulKg _)).
+  by rewrite -[LHS](centsP cHbH')// ?mem_commg ?mem_rVabelem.
 have{cEE} [F [outF [inF outFK inFK] E_F]]:
   {F : finFieldType & {outF : {rmorphism F -> 'M(Hbar)%Mg}
    & {inF : {additive _ -> _} | cancel outF inF & {in E_U, cancel inF outF}}
@@ -1014,6 +1015,11 @@ have sW1_Imu i: W1 \subset 'I[theta (mu_f i) %% H0]%CF.
   rewrite -(cfResE _ (sH1wH _ W1w1w)) -?mem_conjg -?conjsgM ?mulgKV ?H1x //.
   rewrite -(cfResE _ (sH1wH _ W1w1)) ?H1x ?cfBigdprodKabelian //.
   rewrite !ffunE W1w1 W1w1w -[x w1](conjgKV w1) -conjgM !isom_IirrE.
+  pose RR := @cfIsomE _ _ _ _ _ (isoJ (w1 * (inMb w)^-1)%g) 'chi_i.
+  clearbody RR.
+  rewrite /reverse_coercion in RR.
+  rewrite RR.
+  rewrite [LHS]cfIsomE.
   by rewrite !cfIsomE -?mem_conjg ?H1x.
 have inj_mu: {in predC1 0 &, injective (fun i => cfIirr (mk_mu i))}.
   move=> i1 i2 nz_i1 nz_i2 /(congr1 (tnth (irr HU))).