Port to new rewrite goals order

Author: proux01

theories/BGappendixAB.v

@@ -56,7 +56,7 @@ suffices IH gT (E : {group gT}) x y (G := <<[set x; y]>>) :
   apply/subsetP=> _ /morphimP[x Nx Ax ->]; have NGx := subsetP sANG x Ax.
   apply: Baer_Suzuki => [|_ /morphimP[y Ny NGy ->]]; first exact: mem_quotient.
   rewrite -morphJ // -!morphim_set1 -?[<<_>>]morphimY ?sub1set ?groupJ //.
-  set G1 := _ <*> _; rewrite /pgroup -(card_isog (second_isog _)); last first.
+  set G1 := _ <*> _; rewrite /pgroup -(card_isog (second_isog _)).
     by rewrite join_subG !sub1set Nx groupJ.
   have{Nx NGx Ny NGy} [[Gx Nx] [Gy Ny]] := (setIP NGx, setIP NGy).
   have sG1G: G1 \subset G by rewrite join_subG !sub1set groupJ ?andbT.
@@ -505,8 +505,3 @@ by rewrite TI_cardMg ?mulnK //; apply/trivgP; rewrite /= setIC -tiSD setSI.
 Qed.
 
 End Puig_factorization.
-
-
-
-
-

theories/BGappendixC.v

@@ -162,7 +162,7 @@ have /cyclicP[u0 defFU]: cyclic [set: {unit F}] by apply: cycFU.
 have o_u0: #[u0] = (p ^ q).-1 by rewrite orderE -defFU card_finField_unit oF.
 have ->: psi @: U = uval @: (sigmaU @* U) by rewrite morphimEdom -imset_comp.
 have /set1P[->]: (sigmaU @* U)%G \in [set <[u0 ^+ (#[u0] %/ nU)]>%G].
-  rewrite -cycle_sub_group ?inE; last first.
+  rewrite -cycle_sub_group ?inE.
     by rewrite o_u0 -(divnK (dvdn_pred_predX p q)) dvdn_mulr.
   by rewrite -defFU subsetT card_injm //= oU.
 rewrite divnA ?dvdn_pred_predX // -o_u0 mulKn //.
@@ -198,7 +198,7 @@ have oFpU: #|galFpU| = p.-1.
   rewrite card_injm ?card_finField_unit ?oF_p //.
   by apply/injmP=> v1 v2 _ _ []/(fmorph_inj (in_alg F))/val_inj.
 have oUU: #|sigmaU @* U| = nU by rewrite card_injm.
-rewrite dprodE ?coprime_TIg ?oUU ?oFpU //; last first.
+rewrite dprodE ?coprime_TIg ?oUU ?oFpU //.
   by rewrite (sub_abelian_cent2 (cyclic_abelian (cycFU [set: _]))) ?subsetT.
 apply/eqP; rewrite eqEcard subsetT coprime_cardMg oUU oFpU //=.
 by rewrite card_finField_unit oF divnK ?dvdn_pred_predX.
@@ -274,8 +274,8 @@ have sizePa: size Pa = q.+1.
   have sizePaX (beta : {rmorphism F -> F}) : size (beta (1 - a) *: 'X + 1) = 2%N.
     rewrite -mul_polyC size_MXaddC oner_eq0 andbF size_polyC fmorph_eq0.
     by rewrite subr_eq0 eq_sym (negbTE not_a1).
-  rewrite size_prod => [|i _]; last by rewrite -size_poly_eq0 sizePaX.
-  rewrite (eq_bigr (fun _ => 2%N)) => [|beta _]; last by rewrite sizePaX.
+  rewrite size_prod => [i _|]; first by rewrite -size_poly_eq0 sizePaX.
+  rewrite (eq_bigr (fun _ => 2%N)) => [beta _|]; first by rewrite sizePaX.
   rewrite sum_nat_const muln2 -addnn -addSn addnK.
   by rewrite -galois_dim ?finField_galois ?subvf // dimv1 divn1 dimFpq.
 have sizePa1: size (Pa - 1) = q.+1.
@@ -302,7 +302,7 @@ have [q_gt4 | q_le4] := ltnP 4 q.
   have ->: #|E| = e.
     rewrite /e /gring_classM_coef !inK_E ?groupX //.
     transitivity #|[set u in U | s^-1 ^ u * s ^+ 2 \in s ^: U]%g|.
-      rewrite -(card_in_imset (sub_in2 _ inj_psi)) => [|u /setIdP[] //].
+      rewrite -(card_in_imset (sub_in2 _ inj_psi)) => [u /setIdP[] //|].
       apply: eq_card => x; rewrite inE -!im_psi.
       apply/andP/imsetP=> [[/imsetP[u Uu ->] /imsetP[v Uv Dv]]{x} | ].
         exists u; rewrite // inE Uu /=; apply/imsetP; exists v => //.
@@ -312,7 +312,7 @@ have [q_gt4 | q_le4] := ltnP 4 q.
       by rewrite Dv !imset_f.
     rewrite DsH (DsH 1%N) expg1; have [w Uw ->] := repr_class U (s ^+ 2).
     pose f u := (s ^ (u * w), (s^-1 ^ u * s ^+ 2) ^ w).
-    rewrite -(@card_in_imset _ _ f) => [|u v]; last first.
+    rewrite -(@card_in_imset _ _ f) => [u v|].
       by move=> /setIdP[Uu _] /setIdP[Uv _] [/injJU/mulIg-> //]; apply: groupM.
     apply: eq_card => [[x1 x2]]; rewrite inE -andbA.
     apply/imsetP/and3P=> [[u /setIdP[Uu sUs2u'] [-> ->]{x1 x2}] | []].
@@ -598,7 +598,7 @@ have sUs_modP m a j n u s1 v: is_sUs m a j n u s1 v -> a ^ t ^+ j = u * v.
   have [nUP /isom_inj/injmP/=quoUP_inj] := sdprod_isom defH.
   case=> Ua Uu Uv P0s1 /(congr1 (coset P)); rewrite (conjgCV u) -(mulgA _ u).
   rewrite coset_kerr ?groupV ?groupX //.
-  rewrite coset_kerl ?groupX // [RHS]coset_kerl; last first.
+  rewrite coset_kerl ?groupX // [RHS]coset_kerl.
     by rewrite -mem_conjg (normsP nUP) // (subsetP sP0P).
   by move/quoUP_inj->; rewrite ?nUtn ?groupM.
 have expUMp u v Uu Uv := expgMn p (centsP cUU u v Uu Uv).

theories/BGsection1.v

@@ -270,12 +270,12 @@ Proposition coprime_cent_Fitting gT (A G : {group gT}) :
   'C_A('F(G)) \subset 'C(G).
 Proof.
 move=> nGA coGA solG; apply: subset_trans (subsetIr A _); set C := 'C_A(G).
-rewrite -quotient_sub1 /= -/C; last first.
+rewrite -quotient_sub1 /= -/C.
   by rewrite subIset // normsI ?normG // norms_cent.
 apply: subset_trans (quotient_subcent _ _ _) _; rewrite /= -/C.
 have nCG: G \subset 'N(C) by rewrite cents_norm // centsC subsetIr.
 rewrite /= -(setIidPr (Fitting_sub _)) -[(G :&: _) / _](morphim_restrm nCG).
-rewrite injmF //=; last first.
+rewrite injmF //=.
   by rewrite ker_restrm ker_coset setIA (coprime_TIg coGA) subIset ?subxx.
 rewrite morphim_restrm -quotientE setIid.
 rewrite coprime_trivg_cent_Fitting ?quotient_norms ?coprime_morph //=.
@@ -325,7 +325,7 @@ Proposition coprime_commGid gT (A G : {group gT}) :
 Proof.
 move=> nGA coGA solG; apply/eqP; rewrite eqEsubset commSg ?commg_subl //.
 have nAC: 'C_G(A) \subset 'N(A) by rewrite subIset ?cent_sub ?orbT.
-rewrite -{1}(coprime_cent_prod nGA) // commMG //=; first 1 last.
+rewrite -{1}(coprime_cent_prod nGA) // commMG //=.
   by rewrite !normsR // subIset ?normG.
 by rewrite (commG1P (subsetIr _ _)) mulg1.
 Qed.
@@ -523,7 +523,7 @@ elim: i x Hx => [|[|i] IHi] x Hx xp1.
 have expH': {in H &, forall y z, [~ y, z] ^+ p = 1}.
   move=> y z Hy Hz; apply/eqP.
   have /setIP[_ cHyz]: [~ y, z] \in 'Z(H) by rewrite (subsetP clH) // mem_commg.
-  rewrite -commXg; last exact/commute_sym/(centP cHyz).
+  rewrite -commXg; first exact/commute_sym/(centP cHyz).
   suffices /setIP[_ cHyp]: y ^+ p \in 'Z(H) by apply/commgP/(centP cHyp).
   rewrite (subsetP sPhiZ) // (Phi_joing pH) mem_gen // inE orbC.
   by rewrite (Mho_p_elt 1) ?(mem_p_elt pH).
@@ -626,7 +626,7 @@ Proof.
 move=> solG P sylP; have [sPO pP _] := and3P sylP; pose K := 'O_p^'(G).
 have nKG: G \subset 'N(K) by rewrite normal_norm ?pcore_normal.
 have nKC: 'C_G(P) \subset 'N(K) by rewrite subIset ?nKG.
-rewrite -(quotientSGK nKC) //; last first.
+rewrite -(quotientSGK nKC) //.
   by rewrite /= -pseries1 (pseries_sub_catl [::_]).
 apply: subset_trans (quotient_subcent _ _ _) _; rewrite /= -/K.
 suffices ->: P / K = 'O_p(G / K).
@@ -687,7 +687,7 @@ without loss p'G1: gT G R sRG pR solG / 'O_p^'(G) = 1.
   have nOG_CR: 'C_G(R) \subset 'N('O_p^'(G)) by rewrite subIset ?gFnorm.
   move=> IH; rewrite -quotient_sub1 ?gFsub_trans //.
   apply: subset_trans (morphimF _ _ nOG_CR) _; rewrite /= -quotientE.
-  rewrite -(coprime_subcent_quotient_pgroup pR) ?pcore_sub //; first 1 last.
+  rewrite -(coprime_subcent_quotient_pgroup pR) ?pcore_sub //.
   - by rewrite (subset_trans sRG) ?gFnorm.
   - by rewrite coprime_sym (pnat_coprime _ (pcore_pgroup _ _)).
   have p'Gq1 : 'O_p^'(G / 'O_p^'(G)) = 1 := trivg_pcore_quotient p^' G.
@@ -731,15 +731,15 @@ without loss nilG: G nGA coGA leGn / nilpotent G.
   move=> {} IHn; apply/eqP; rewrite eqEsubset gen_subG.
   apply/andP; split; last by apply/bigcupsP=> B _; apply: subsetIl.
   pose T := [set P : {group gT} | Sylow G P & A \subset 'N(P)].
-  rewrite -{1}(@Sylow_transversal_gen _ T G) => [|P | p _]; first 1 last.
+  rewrite -{1}(@Sylow_transversal_gen _ T G) => [P | p _|].
   - by rewrite inE -!andbA; case/and4P.
   - have [//|P sylP nPA] := sol_coprime_Sylow_exists p (abelian_sol abelA) nGA.
     by exists P; rewrite ?inE ?(p_Sylow sylP).
   rewrite gen_subG; apply/bigcupsP=> P {T}/setIdP[/SylowP[p _ sylP] nPA].
   have [sPG pP _] := and3P sylP.
   rewrite (IHn P) ?(pgroup_nil pP) ?(coprimeSg sPG) ?genS //.
-    by apply/bigcupsP=> B cycBq; rewrite (bigcup_max B) ?setSI.
-  by rewrite (leq_trans (subset_leq_card sPG)).
+    by rewrite (leq_trans (subset_leq_card sPG)).
+  by apply/bigcupsP=> B cycBq; rewrite (bigcup_max B) ?setSI.
 apply/eqP; rewrite eqEsubset gen_subG.
 apply/andP; split; last by apply/bigcupsP=> B _; apply: subsetIl.
 have [Z1 | ntZ] := eqsVneq 'Z(G) 1.
@@ -756,7 +756,7 @@ set GC := <<_>>; have sMGC: M \subset GC.
   exact/abelem_mx_irrP.
 rewrite -(quotientSGK nMG sMGC).
 have: A / M \subset 'N(G / M) by rewrite morphim_norms.
-move/IHn->; rewrite ?morphim_abelian ?coprime_morph {IHn}//; first 1 last.
+move/IHn->; rewrite ?morphim_abelian ?coprime_morph {IHn}//.
   by rewrite (leq_trans _ leGn) ?ltn_quotient.
 rewrite gen_subG; apply/bigcupsP=> Bq; rewrite andbC => /andP[].
 have: M :&: A = 1 by rewrite coprime_TIg.
@@ -986,15 +986,15 @@ case/and3P: pV => pV abV; have cUV := subset_trans sUV abV.
 have sVVG := joing_subl V G.
 have{nUG} nUVG: U <| V <*> G.
   by rewrite /(U <| _) join_subG (subset_trans sUV) // cents_norm // centsC.
-rewrite -{nUVG}(Gaschutz_split nUVG) ?(abelianS sUV) // in splitU; last first.
+rewrite -{nUVG}(Gaschutz_split nUVG) ?(abelianS sUV) // in splitU.
   rewrite -divgS ?joing_subl //= norm_joinEr //.
   have coVG: coprime #|V| #|G| := pnat_coprime pV p'G.
   by rewrite coprime_cardMg // mulnC mulnK // (coprimeSg sUV).
 case/splitsP: splitU => WG /complP[tiUWG /= defVG].
 exists (WG :&: V)%G.
-  rewrite dprodE; last by rewrite setIA tiUWG (setIidPl _) ?sub1G.
-    by rewrite group_modl // defVG (setIidPr _).
-  by rewrite subIset // orbC centsC cUV.
+  rewrite dprodE; [|by rewrite setIA tiUWG (setIidPl _) ?sub1G|].
+    by rewrite subIset // orbC centsC cUV.
+  by rewrite group_modl // defVG (setIidPr _).
 rewrite (subset_trans (joing_subr V _)) // -defVG mul_subG //.
    by rewrite cents_norm ?(subset_trans cUV) ?centS ?subsetIr.
 rewrite normsI ?normG // (subset_trans (mulG_subr U _)) //.
@@ -1087,12 +1087,12 @@ Lemma pquo_plength1 G H :
 Proof.
 rewrite /plength_1 => nHG pH trO; apply/idP/idP; last exact: plength1_quo.
 rewrite (pseries_pop _ trO) => pGH1; rewrite eqEsubset pseries_sub /=.
-rewrite pseries_pop //; last first.
+rewrite pseries_pop //.
   apply/eqP; rewrite -subG1; have <-: H :&: 'O_p^'(G) = 1.
     by apply: coprime_TIg; apply: pnat_coprime (pcore_pgroup _ _).
   rewrite setIC subsetI subxx -quotient_sub1.
-    by rewrite -trO morphim_pcore.
-  exact/gFsub_trans/normal_norm.
+    exact/gFsub_trans/normal_norm.
+  by rewrite -trO morphim_pcore.
 have nOG: 'O_{p}(G) <| G by apply: pseries_normal.
 rewrite -(quotientSGK (normal_norm nOG)) ?(pseries_sub_catl [:: _]) //.
 have [|f f_inj im_f] := third_isom _ nHG nOG.
@@ -1124,7 +1124,7 @@ apply/idP/idP=> [p1G | pU].
   apply: (@pnat_dvd _ #|p_elt_gen p G : 'O_p^'(G)|).
     by rewrite -[#|_ : 'O_p^'(G)|]indexgI indexgS ?pcoreS.
   apply: (@pnat_dvd _ #|'O_p(G / 'O_{p^'}(G))|); last exact: pcore_pgroup.
-  rewrite -card_quotient; last first.
+  rewrite -card_quotient.
     by rewrite (subset_trans sUG) // normal_norm ?pcore_normal.
   rewrite -quotient_pseries pseries1 cardSg ?morphimS //=.
   rewrite gen_subG; apply/subsetP=> x; rewrite inE; case/andP=> Gx p_x.
@@ -1172,8 +1172,8 @@ have exB (N : {group gT}) :
            forall x, x \in B -> #[x] = p -> x \in N
          & forall Q : {group gT}, p^'.-subgroup(U) Q -> Q \subset B].
 - move=> nsNG; have [sNG nNG] := andP nsNG.
-  rewrite p_elt_gen_length1 // (_ : p_elt_gen _ _ = U / N); last first.
-    rewrite /quotient morphim_gen -?quotientE //; last first.
+  rewrite p_elt_gen_length1 // (_ : p_elt_gen _ _ = U / N).
+    rewrite /quotient morphim_gen -?quotientE //.
       by rewrite setIdE subIset ?nNG.
     congr <<_>>; apply/setP=> Nx; rewrite inE setIdE quotientGI // inE.
     apply: andb_id2l => /morphimP[x NNx Gx ->{Nx}] /=.
@@ -1190,7 +1190,7 @@ have exB (N : {group gT}) :
   - by rewrite (subset_trans (sub_gen _) nB) ?subsetUl.
   - have nNx: x \in 'N(N) by rewrite (subsetP nN_UN) ?(subsetP sB).
     apply: coset_idr => //; rewrite -[coset N x](consttC p).
-    rewrite !(constt1P _) ?mulg1 // ?p_eltNK.
+    rewrite !(constt1P _) ?mulg1 // ?p_eltNK; last first.
       by rewrite morph_p_elt // /p_elt p_x pnat_id.
     have: coset N x \in B / N by apply/morphimP; exists x.
     by apply: mem_p_elt; rewrite /= -defB pcore_pgroup.

theories/BGsection10.v

@@ -295,7 +295,7 @@ have M0C_M1: gval M1 \in orbit 'Js 'C(X) M0.
   by rewrite (atransP (IHX _ ltXX1 pX1)) inE ?MG_M0 //; case/setIdP: O_M1 => ->.
 have M0tC_M2: M2 \in orbit 'Js 'C(X) (M0 :^ t).
   rewrite (subsetP (imsetS _ (centS (proper_sub ltXX2)))) // -orbitE.
-  rewrite (atransP (IHX _ ltXX2 pX2)) inE; first by case/setIdP: O_M2 => ->.
+  rewrite (atransP (IHX _ ltXX2 pX2)) inE; last by case/setIdP: O_M2 => ->.
   rewrite (acts_act (acts_orbit _ _ _)) ?inE ?MG_M0 //.
   by rewrite (subset_trans sX2Pt) ?conjSg.
 rewrite (orbit_eqP M0C_M1) (orbit_transl _ M0tC_M2).
@@ -309,15 +309,15 @@ have pl1L: p.-length_1 L.
   by case/rank2_der1_complement; rewrite ?mFT_sol ?plength1_pseries2_quo.
 have [|u v nLPu Lp'_v ->] := imset2P (_ : t \in 'N_L(P) * 'O_p^'(L)).
   by rewrite normC ?plength1_Frattini // subIset ?gFnorm.
-rewrite actM (orbit_transl _ (mem_orbit _ _ _)); last first.
+rewrite actM (orbit_transl _ (mem_orbit _ _ _)).
   have coLp'X: coprime #|'O_p^'(L)| #|X| := p'nat_coprime (pcore_pgroup _ _) pX.
   apply: subsetP Lp'_v; have [sLp'L nLp'L] := andP (pcore_normal p^' L).
   rewrite -subsetIidl -coprime_norm_cent ?subsetIidl //.
   exact: subset_trans (normG X) nLp'L.
 have [|w x nM0Pw cPx ->] := imset2P (_ : u \in 'N_M0(P) * 'C(P)).
-  rewrite normC ?part_c ?IHX //; first by case/setIP: nLPu.
+  rewrite normC ?part_c ?IHX //; last by case/setIP: nLPu.
   by rewrite setIC subIset ?cent_norm.
-rewrite actM /= (@conjGid _ M0) ?mem_orbit //; last by case/setIP: nM0Pw.
+rewrite actM /= (@conjGid _ M0) ?mem_orbit //; first by case/setIP: nM0Pw.
 by rewrite (subsetP (centS (subset_trans (proper_sub ltXX1) sX1P))).
 Qed.
 
@@ -401,7 +401,7 @@ Theorem Msigma_Hall : \sigma(M).-Hall(M) M`_\sigma.
 Proof.
 have [H hallH] := Hall_exists \sigma(M) solM; have [sHM sH _] := and3P hallH.
 rewrite /M`_\sigma (normal_Hall_pcore hallH) // -(quotientGK nsMaM).
-rewrite -(quotientGK (normalS _ sHM nsMaM)) ?cosetpre_normal //; last first.
+rewrite -(quotientGK (normalS _ sHM nsMaM)) ?cosetpre_normal //.
   by rewrite (subset_trans sMaMs) ?pcore_sub_Hall.
 have hallHa: \sigma(M).-Hall(F) (H / M`_\alpha).
   apply: pHall_subl (subset_trans _ Malpha_quo_sub_Fitting) (Fitting_sub _) _.
@@ -424,7 +424,7 @@ rewrite pHallE subsetT /= eqn_dvd {1}(card_Hall Msigma_Hall).
 rewrite partn_dvd ?cardG_gt0 ?cardSg ?subsetT //=.
 apply/dvdn_partP; rewrite ?part_gt0 // => p.
 rewrite pi_of_part ?cardG_gt0 // => /andP[_ s_p].
-rewrite partn_part => [|q /eqnP-> //].
+rewrite partn_part => [q /eqnP-> //|].
 have [P sylP] := Sylow_exists p M; have [sPM pP _] := and3P sylP.
 rewrite -(card_Hall (sigma_Sylow_G _ _ sylP)) ?cardSg //.
 by rewrite (sub_Hall_pcore Msigma_Hall) ?(pi_pgroup pP).
@@ -519,7 +519,7 @@ Proof.
 apply: contraL => /= s_p; have piMp := sigma_sub_pi maxM s_p.
 have p_pr: prime p by move: piMp; rewrite mem_primes; case/andP.
 rewrite -p'natE ?(pi'_p'nat _ s_p) // -pgroupE -partG_eq1.
-rewrite -(card_Hall (quotient_pHall _ Msigma_Hall)) /=; last first.
+rewrite -(card_Hall (quotient_pHall _ Msigma_Hall)) /=.
   exact/gFsub_trans/gFnorm.
 by rewrite quotientS1 ?cards1 // Msigma_der1.
 Qed.
@@ -934,7 +934,7 @@ do [move: sWXM'; rewrite (joing_idPr (pHall_sub sylX)) => sWM'] in hallW.
 have nMbX: X \subset 'N(M`_\beta) := subset_trans sXM (normal_norm nsMbM).
 have nsMbXM : M`_\beta <*> X <| M.
   rewrite -{2}(quotientGK nsMbM) -quotientYK ?cosetpre_normal //=.
-  rewrite (eq_Hall_pcore _ (quotient_pHall nMbX sylX)); last first.
+  rewrite (eq_Hall_pcore _ (quotient_pHall nMbX sylX)).
     exact: nilpotent_pcore_Hall Mbeta_quo_nil.
   by rewrite gFnormal_trans ?quotient_normal ?gFnormal.
 pose U := 'N_M(X); have defM: M`_\beta * U = M.
@@ -972,7 +972,7 @@ have nMbS := subset_trans sSM (normal_norm nsMbM).
 have nMbSM: M`_\beta <*> S <| M.
   rewrite -{2}(quotientGK nsMbM) -quotientYK ?cosetpre_normal //=.
   have sylS_M' := pHall_subl sSM' sM'M sylS.
-  rewrite (eq_Hall_pcore _ (quotient_pHall nMbS sylS_M')); last first.
+  rewrite (eq_Hall_pcore _ (quotient_pHall nMbS sylS_M')).
     exact: nilpotent_pcore_Hall Mbeta_quo_nil.
   by rewrite gFnormal_trans ?quotient_normal ?gFnormal.
 have defM: M`_\beta * 'N_M(S) = M.
@@ -1191,8 +1191,8 @@ have nilK0Ms: nilpotent (K0 <*> M`_\sigma).
   apply: (prime_Frobenius_sol_kernel_nil mulK0MsP); rewrite ?oP //=.
     by rewrite (solvableS _ solM) // !join_subG sK0M pcore_sub.
   rewrite norm_joinEl // -subcent_TImulg ?subsetI ?nK0P //.
-    by rewrite coprime_abel_cent_TI ?mul1g.
-  exact: coprime_TIg.
+    exact: coprime_TIg.
+  by rewrite coprime_abel_cent_TI ?mul1g.
 have cMsK0: K0 \subset 'C(M`_\sigma).
   rewrite (sub_nilpotent_cent2 nilK0Ms) ?joing_subl ?joing_subr //.
   exact: pnat_coprime (pcore_pgroup _ _) sg'K0.
@@ -1344,15 +1344,15 @@ have [Y [{cplA1C} cycY sZ0Y defC cCC]]: exists Y, cplA1C Y.
   have pE := pgroupS sES pS.
   have defS1: 'Ohm_1(S) = E.
     apply/eqP; rewrite (OhmE 1 pS) eqEsubset gen_subG andbC.
-    rewrite sub_gen; last by rewrite subsetI sES sub_LdivT.
+    rewrite sub_gen; first by rewrite subsetI sES sub_LdivT.
     apply/subsetP=> ey /LdivP[]; rewrite -mulEY.
     case/imset2P=> e y Ee Yy -> eyp; rewrite groupM //.
     rewrite (subsetP (center_sub E)) // -defY1 (OhmE 1 pY) mem_gen //.
-    rewrite expgMn in eyp; last by red; rewrite -(centsP cEY).
+    rewrite expgMn in eyp; first by red; rewrite -(centsP cEY).
     by rewrite (exponentP eE) // mul1g in eyp; rewrite !inE Yy eyp eqxx.
   have sAE: A \subset E by rewrite -defS1 -(Ohm1_id abelA) OhmS.
   have defC: A * Y = C.
-    rewrite /C -mulEY setIC -group_modr; last first.
+    rewrite /C -mulEY setIC -group_modr.
       by rewrite -defY subIset // orbC centS.
     congr (_ * _); apply/eqP; rewrite /= setIC eqEcard subsetI sAE.
     have pCEA: p.-group 'C_E(A) := pgroupS (subsetIl E _) pE.
@@ -1370,7 +1370,7 @@ have [Y [{cplA1C} cycY sZ0Y defC cCC]]: exists Y, cplA1C Y.
   have{} EpA1 := EpA1 (card_pnElem EpZ1).
   have [sA1A _ oA1] := pnElemPcard EpA1.
   have [_ defA _ tiA1Z] := dprodP (p2Elem_dprodP Ep2A EpA1 EpZ1 neqA1Z).
-  exists Y; split; rewrite // dprodE ?(centSS _ sA1A cAY) ?prime_TIg ?oA1 //.
+  exists Y; split; rewrite // dprodE ?(centSS _ sA1A cAY) ?prime_TIg ?oA1 //; last first.
     by rewrite -(mulSGid sZ0Y) -eqZ10 mulgA defA.
   apply: contraL cycY => sA1Y; rewrite abelian_rank1_cyclic // -ltnNge.
   by rewrite -dimA -rank_abelem ?rankS // -defA eqZ10 mul_subG.
@@ -1386,11 +1386,11 @@ split=> //; first exists (P :&: Y)%G.
   have{defC} [_ defC cA1Y tiA1Y] := dprodP defC.
   rewrite setIC -{2}(setIidPr sPS) setIAC.
   apply: dprod_modl (subset_trans sA0A sAP); rewrite -defC dprodE /=.
-  - by rewrite -(mulSGid sZ0Y) !mulgA mulA0Z defA.
   - rewrite (centSS (subxx Y) sA0A) // -defA centM subsetI cA1Y /=.
     by rewrite sub_abelian_cent ?cyclic_abelian.
-  rewrite setIC -(setIidPr sA0A) setIA -defA -group_modr //.
-  by rewrite (setIC Y) tiA1Y mul1g setIC.
+  - rewrite setIC -(setIidPr sA0A) setIA -defA -group_modr //.
+    by rewrite (setIC Y) tiA1Y mul1g setIC.
+  - by rewrite -(mulSGid sZ0Y) !mulgA mulA0Z defA.
 apply/imsetP; exists A1; first by rewrite 2!inE neqA1Z.
 apply/eqP; rewrite eq_sym eqEcard; apply/andP; split.
   apply/subsetP=> _ /imsetP[x /setIP[Px nAx] ->].
@@ -1400,9 +1400,9 @@ apply/eqP; rewrite eq_sym eqEcard; apply/andP; split.
 have pN: p.-group 'N_P(_) := pgroupS (subsetIl P _) pP.
 have defCPA: 'N_('N_P(A))(A1) = 'C_P(A).
   apply/eqP; rewrite eqEsubset andbC subsetI setIS ?cent_sub //.
-  rewrite subIset /=; last by rewrite orbC cents_norm ?centS.
+  rewrite subIset /=; first by rewrite orbC cents_norm ?centS.
   rewrite setIAC (subset_trans (subsetIl _ _)) //= subsetI subsetIl /=.
-  rewrite -defA centM subsetI andbC subIset /=; last first.
+  rewrite -defA centM subsetI andbC subIset /=.
     by rewrite centsC gFsub_trans ?subsetIr.
   have nC_NP: 'N_P(A1) \subset 'N('C(A1)) by rewrite norms_cent ?subsetIr.
   rewrite -quotient_sub1 // subG1 trivg_card1.
@@ -1498,5 +1498,3 @@ by rewrite (sub_mmax_proper maxM).
 Qed.
 
 End Ten.
-
-