New generalised induction idiom (#434)

Replaced the legacy generalised induction idiom with a more robust one
that does not rely on the `{-2}` numerical occurrence selector, using
either new helper lemmas `ubnP` and `ltnSE` or a specific `nat`
induction principle `ltn_ind`.

Added (non-strict in)equality induction helper lemmas

  Added `ubnP[lg]?eq` helper lemmas that abstract an integer expression
along with some (in)equality, in preparation for some generalised
induction. Note that while `ubnPleq` is very similar to `ubnP` (indeed
`ubnP M` is basically `ubnPleq M.+1`), `ubnPgeq` is used to remember
that the inductive value remains below the initial one.
  Used the change log to give notice to users to update the generalised
induction idioms in their proofs to one of the new forms before
Mathcomp 1.11.

11 files changed, 104 insertions, 121 deletions

diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 8c2badb..bfdafae 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -1541,12 +1541,13 @@ Implicit Types (p : nat) (G H K E : {group gT}).
 Lemma abelian_splits x G :
   x \in G -> #[x] = exponent G -> abelian G -> [splits G, over <[x]>].
 Proof.
-move=> Gx ox cGG; apply/splitsP; move: {2}_.+1 (ltnSn #|G|) => n.
-elim: n gT => // n IHn aT in x G Gx ox cGG *; rewrite ltnS => leGn.
+move=> Gx ox cGG; apply/splitsP; have [n] := ubnP #|G|.
+elim: n gT => // n IHn aT in x G Gx ox cGG * => /ltnSE-leGn.
 have: <[x]> \subset G by [rewrite cycle_subG]; rewrite subEproper.
-case/predU1P=> [<-|]; first by exists 1%G; rewrite inE -subG1 subsetIr mulg1 /=.
-case/properP=> sxG [y]; elim: {y}_.+1 {-2}y (ltnSn #[y]) => // m IHm y.
-rewrite ltnS => leym Gy x'y; case: (trivgVpdiv <[y]>) => [y1 | [p p_pr p_dv_y]].
+case/predU1P=> [<- | /properP[sxG [y]]].
+  by exists 1%G; rewrite inE -subG1 subsetIr mulg1 /=.
+have [m] := ubnP #[y]; elim: m y => // m IHm y /ltnSE-leym Gy x'y.
+case: (trivgVpdiv <[y]>) => [y1 | [p p_pr p_dv_y]].
   by rewrite -cycle_subG y1 sub1G in x'y.
 case x_yp: (y ^+ p \in <[x]>); last first.
   apply: IHm (negbT x_yp); rewrite ?groupX ?(leq_trans _ leym) //.
@@ -1558,7 +1559,7 @@ have{x_yp} xp_yp: (y ^+ p \in <[x ^+ p]>).
   rewrite cycle_subG orderXdiv // divnA // mulnC ox.
   by rewrite -muln_divA ?dvdn_exponent ?expgM 1?groupX ?cycle_id.
 have: p <= #[y] by rewrite dvdn_leq.
-rewrite leq_eqVlt; case/predU1P=> [{xp_yp m IHm leym}oy | ltpy]; last first.
+rewrite leq_eqVlt => /predU1P[{xp_yp m IHm leym}oy | ltpy]; last first.
   case/cycleP: xp_yp => k; rewrite -expgM mulnC expgM => def_yp.
   suffices: #[y * x ^- k] < m.
     by move/IHm; apply; rewrite groupMr // groupV groupX ?cycle_id.
@@ -1591,8 +1592,8 @@ Qed.
 
 Lemma abelem_splits p G H : p.-abelem G -> H \subset G -> [splits G, over H].
 Proof.
-elim: {G}_.+1 {-2}G H (ltnSn #|G|) => // m IHm G H.
-rewrite ltnS => leGm abelG sHG; case: (eqsVneq H 1) => [-> | ].
+have [m] := ubnP #|G|; elim: m G H => // m IHm G H /ltnSE-leGm abelG sHG.
+have [-> | ] := eqsVneq H 1. 
   by apply/splitsP; exists G; rewrite inE mul1g -subG1 subsetIl /=.
 case/trivgPn=> x Hx ntx; have Gx := subsetP sHG x Hx.
 have [_ cGG eGp] := and3P abelG.
@@ -1630,10 +1631,11 @@ Definition abelian_type (A : {set gT}) := abelian_type_rec #|A| <<A>>.
 
 Lemma abelian_type_dvdn_sorted A : sorted [rel m n | n %| m] (abelian_type A).
 Proof.
-set R := SimplRel _; pose G := <<A>>%G.
-suffices: path R (exponent G) (abelian_type A) by case: (_ A) => // m t /andP[].
-rewrite /abelian_type -/G; elim: {A}#|A| G {2 3}G (subxx G) => // n IHn G M sGM.
-simpl; case: ifP => //= /andP[cGG ntG]; rewrite exponentS ?IHn //=.
+set R := SimplRel _; pose G := <<A>>%G; pose M := G.
+suffices: path R (exponent M) (abelian_type A) by case: (_ A) => // m t /andP[].
+rewrite /abelian_type -/G; have: G \subset M by [].
+elim: {A}#|A| G M => //= n IHn G M sGM.
+case: andP => //= -[cGG ntG]; rewrite exponentS ?IHn //=.
 case: (abelian_type_subproof G) => H /= [//| x _] /dprodP[_ /= <- _ _].
 exact: mulG_subr.
 Qed.
@@ -1656,10 +1658,9 @@ Theorem abelian_structure G :
     abelian G ->
   {b | \big[dprod/1]_(x <- b) <[x]> = G & map order b = abelian_type G}.
 Proof.
-rewrite /abelian_type genGidG.
-elim: {G}#|G| {-2 5}G (leqnn #|G|) => /= [|n IHn] G leGn cGG.
-  by rewrite leqNgt cardG_gt0 in leGn.
-rewrite {1}cGG /=; case: ifP => [ntG|/eqP->]; last first.
+rewrite /abelian_type genGidG; have [n] := ubnPleq #|G|.
+elim: n G => /= [|n IHn] G leGn cGG; first by rewrite leqNgt cardG_gt0 in leGn.
+rewrite [in _ && _]cGG /=; case: ifP => [ntG|/eqP->]; last first.
   by exists [::]; rewrite ?big_nil.
 case: (abelian_type_subproof G) => H /= [//|x ox xdefG]; rewrite -ox.
 have [_ defG cxH tixH] := dprodP xdefG.
@@ -1675,7 +1676,7 @@ Lemma count_logn_dprod_cycle p n b G :
     \big[dprod/1]_(x <- b) <[x]> = G ->
   count [pred x | logn p #[x] > n] b = logn p #|'Ohm_n.+1(G) : 'Ohm_n(G)|.
 Proof.
-have sOn1 := @Ohm_leq gT _ _ _ (leqnSn n).
+have sOn1 H: 'Ohm_n(H) \subset 'Ohm_n.+1(H) by apply: Ohm_leq.
 pose lnO i (A : {set gT}) := logn p #|'Ohm_i(A)|.
 have lnO_le H: lnO n H <= lnO n.+1 H.
   by rewrite dvdn_leq_log ?cardG_gt0 // cardSg ?sOn1.
@@ -1781,7 +1782,7 @@ rewrite big_cons => defG; rewrite -(dprod_card defG).
 rewrite -(dprod_card (Ohm_dprod n defG)) -(dprod_card (Mho_dprod n defG)) /=.
 rewrite mulnCA -!mulnA mulnCA mulnA; case/dprodP: defG => [[_ H _ defH] _ _ _].
 rewrite defH {b G defH IHb}(IHb H defH); congr (_ * _)%N => {H}.
-elim: {x}_.+1 {-2}x (ltnSn #[x]) => // m IHm x; rewrite ltnS => lexm.
+have [m] := ubnP #[x]; elim: m x => // m IHm x /ltnSE-lexm.
 case p_x: (p_group <[x]>); last first.
   case: (eqVneq x 1) p_x => [-> |]; first by rewrite cycle1 p_group1.
   rewrite -order_gt1 /p_group -orderE; set p := pdiv _ => ntx p'x.
@@ -1804,7 +1805,7 @@ set k := logn p #[x]; have ox: #[x] = (p ^ k)%N by rewrite -card_pgroup.
 case: (leqP k n) => [le_k_n | lt_n_k].
   rewrite -(subnKC le_k_n) subnDA subnn expg1 expnD expgM -ox.
   by rewrite expg_order expg1n order1 muln1.
-rewrite !orderXgcd ox -{-3}(subnKC (ltnW lt_n_k)) expnD.
+rewrite !orderXgcd ox -[in (p ^ k)%N](subnKC (ltnW lt_n_k)) expnD.
 rewrite gcdnC gcdnMl gcdnC gcdnMr.
 by rewrite mulnK ?mulKn ?expn_gt0 ?prime_gt0.
 Qed.
@@ -1823,11 +1824,10 @@ have ->: 'r_p(G) = logn p #|G / K|.
   rewrite p_rank_abelian // card_quotient /= ?gFnorm // -divgS ?Mho_sub //.
   by rewrite -(mul_card_Ohm_Mho_abelian 1 cGG) mulnK ?cardG_gt0.
 case: (grank_witness G) => B genB <-; rewrite -genB.
-have: <<B>> \subset G by rewrite genB.
-elim: {B genB}_.+1 {-2}B (ltnSn #|B|) => // m IHm B; rewrite ltnS.
-case: (set_0Vmem B) => [-> | [x Bx]].
-  by rewrite gen0 quotient1 cards1 logn1.
-rewrite (cardsD1 x) Bx -{2 3}(setD1K Bx); set B' := B :\ x => ltB'm.
+have{genB}: <<B>> \subset G by rewrite genB.
+have [m] := ubnP #|B|; elim: m B => // m IHm B.
+have [-> | [x Bx]] := set_0Vmem B; first by rewrite gen0 quotient1 cards1 logn1.
+rewrite ltnS (cardsD1 x) Bx -[in <<B>>](setD1K Bx); set B' := B :\ x => ltB'm.
 rewrite -joingE -joing_idl -joing_idr -/<[x]> join_subG => /andP[Gx sB'G].
 rewrite cent_joinEl ?(sub_abelian_cent2 cGG) //.
 have nKx: x \in 'N(K) by rewrite -cycle_subG (subset_trans Gx) ?gFnorm.
@@ -1882,10 +1882,11 @@ set e := exponent G => cGG pG /andP[n_gt0 n_lte] eq_Ohm_Mho.
 suffices: all (pred1 e) (abelian_type G).
   by rewrite /homocyclic cGG; apply: all_pred1_constant.
 case/abelian_structure: cGG (abelian_type_gt1 G) => b defG <-.
-elim: b {-3}G defG (subxx G) eq_Ohm_Mho => //= x b IHb H.
+set H := G in defG eq_Ohm_Mho *; have sHG: H \subset G by [].
+elim: b H defG sHG eq_Ohm_Mho => //= x b IHb H.
 rewrite big_cons => defG; case/dprodP: defG (defG) => [[_ K _ defK]].
-rewrite defK => defHm cxK; rewrite setIC; move/trivgP=> tiKx defHd.
-rewrite -{1}defHm {defHm} mulG_subG cycle_subG ltnNge -trivg_card_le1.
+rewrite defK => defHm cxK; rewrite setIC => /trivgP-tiKx defHd.
+rewrite -{}[in H \subset G]defHm mulG_subG cycle_subG ltnNge -trivg_card_le1.
 case/andP=> Gx sKG; rewrite -(Mho_dprod _ defHd) => /esym defMho /andP[ntx ntb].
 have{defHd} defOhm := Ohm_dprod n defHd.
 apply/andP; split; last first.
@@ -1907,7 +1908,7 @@ rewrite eqn_dvd dvdn_exponent //= -ltnNge => lt_x_e.
 rewrite (leq_trans (ltn_Pmull (prime_gt1 p_pr) _)) ?expn_gt0 ?prime_gt0 //.
 rewrite -expnS dvdn_leq // ?gcdn_gt0 ?order_gt0 // dvdn_gcd.
 rewrite pfactor_dvdn // dvdn_exp2l.
-  by rewrite -{2}[logn p _]subn0 ltn_sub2l // lognE p_pr order_gt0 p_dv_x.
+  by rewrite -[xp in _ < xp]subn0 ltn_sub2l // lognE p_pr order_gt0 p_dv_x.
 rewrite ltn_sub2r // ltnNge -(dvdn_Pexp2l _ _ (prime_gt1 p_pr)) -!p_part.
 by rewrite !part_pnat_id // (pnat_dvd (exponent_dvdn G)).
 Qed.
diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v
index d6ada5f..cb86051 100644
--- a/mathcomp/solvable/alt.v
+++ b/mathcomp/solvable/alt.v
@@ -329,47 +329,32 @@ Lemma rfd_odd (p : {perm T}) : p x = x -> rfd p = p :> bool.
 Proof.
 have rfd1: rfd 1 = 1.
   by apply/permP => u; apply: val_inj; rewrite permE /= if_same !perm1.
-have HP0 (t : {perm T}): #|[set x | t x != x]| = 0 -> rfd t = t :> bool.
-- move=> Ht; suff ->: t = 1 by rewrite rfd1 !odd_perm1.
-  apply/permP => z; rewrite perm1; apply/eqP/wlog_neg => nonfix_z.
-  by rewrite (cardD1 z) inE nonfix_z in Ht.
-elim: #|_| {-2}p (leqnn #|[set x | p x != x]|) => {p}[|n Hrec] p Hp Hpx.
-  by apply: HP0; move: Hp; case: card.
-case Ex: (pred0b (mem [set x | p x != x])); first by apply: HP0; move/eqnP: Ex.
-case/pred0Pn: Ex => x1; rewrite /= inE => Hx1.
-have nx1x: x1 != x by apply/eqP => HH; rewrite HH Hpx eqxx in Hx1.
-have npxx1: p x != x1 by apply/eqP => HH; rewrite -HH !Hpx eqxx in Hx1.
-have npx1x: p x1 != x.
-  by apply/eqP; rewrite -Hpx; move/perm_inj => HH; case/eqP: nx1x.
+have [n] := ubnP #|[set x | p x != x]|; elim: n p => // n IHn p le_p_n px_x.
+have [p_id | [x1 Hx1]] := set_0Vmem [set x | p x != x].
+  suffices ->: p = 1 by rewrite rfd1 !odd_perm1.
+  by apply/permP => z; apply: contraFeq (in_set0 z); rewrite perm1 -p_id inE.
+have nx1x: x1 != x by apply: contraTneq Hx1 => ->; rewrite inE px_x eqxx.
+have npxx1: p x != x1 by apply: contraNneq nx1x => <-; rewrite px_x.
+have npx1x: p x1 != x by rewrite -px_x (inj_eq perm_inj).
 pose p1 := p * tperm x1 (p x1).
-have Hp1: p1 x = x.
-  by rewrite /p1 permM; case tpermP => // [<-|]; [rewrite Hpx | move/perm_inj].
-have Hcp1: #|[set x | p1 x != x]| <= n.
-  have F1 y: p y = y -> p1 y = y.
-    move=> Hy; rewrite /p1 permM Hy.
-    by case: tpermP => [<-|/(canLR (permK p))<-|] //; apply/(canLR (permK p)).
-  have F2: p1 x1 = x1 by rewrite /p1 permM tpermR.
-  have F3: [set x | p1 x != x] \subset [predD1 [set x | p x != x] & x1].
-    apply/subsetP => z; rewrite !inE permM.
-    case tpermP => HH1 HH2.
-    - rewrite eq_sym HH1 andbb; apply/eqP=> dx1.
-      by rewrite dx1 HH1 dx1 eqxx in HH2.
-    - by rewrite (perm_inj HH1) eqxx in HH2.
-    by move->; rewrite andbT; apply/eqP => HH3; rewrite HH3 in HH2.
-  apply: (leq_trans (subset_leq_card F3)).
-  by move: Hp; rewrite (cardD1 x1) inE Hx1.
-have ->: p = p1 * tperm x1 (p x1) by rewrite -mulgA tperm2 mulg1.
-rewrite odd_permM odd_tperm eq_sym Hx1 morphM; last 2 first.
-- by rewrite 2!inE; apply/astab1P.
-- by rewrite 2!inE; apply/astab1P; rewrite -{1}Hpx /= /aperm -permM.
-rewrite odd_permM Hrec //=; congr (_ (+) _).
+have fix_p1 y: p y = y -> p1 y = y.
+  by move=> pyy; rewrite permM; have [<-|/perm_inj<-|] := tpermP; rewrite ?pyy.
+have p1x_x: p1 x = x by apply: fix_p1.
+have{le_p_n} lt_p1_n: #|[set x | p1 x != x]| < n.
+  move: le_p_n; rewrite ltnS (cardsD1 x1) Hx1; apply/leq_trans/subset_leq_card.
+  rewrite subsetD1 inE permM tpermR eqxx andbT.
+  by apply/subsetP=> y; rewrite !inE; apply: contraNneq=> /fix_p1->.
+transitivity (p1 (+) true); last first.
+  by rewrite odd_permM odd_tperm -Hx1 inE eq_sym addbK.
+have ->: p = p1 * tperm x1 (p x1) by rewrite -tpermV mulgK.
+rewrite morphM; last 2 first; first by rewrite 2!inE; apply/astab1P.
+  by rewrite 2!inE; apply/astab1P; rewrite -[RHS]p1x_x permM px_x.
+rewrite odd_permM IHn //=; congr (_ (+) _).
 pose x2 : T' := Sub x1 nx1x; pose px2 : T' := Sub (p x1) npx1x.
-suff ->: rfd (tperm x1 (p x1)) = tperm x2 px2.
-  by rewrite odd_tperm -val_eqE eq_sym.
+suffices ->: rfd (tperm x1 (p x1)) = tperm x2 px2.
+  by rewrite odd_tperm eq_sym; rewrite inE in Hx1.
 apply/permP => z; apply/val_eqP; rewrite permE /= tpermD // eqxx.
-case: (tpermP x2) => [->|->|HH1 HH2]; rewrite /x2 ?tpermL ?tpermR 1?tpermD //.
-  by apply/eqP=> HH3; case: HH1; apply: val_inj.
-by apply/eqP => HH3; case: HH2; apply: val_inj.
+by rewrite !permE /= -!val_eqE /= !(fun_if sval) /=.
 Qed.
 
 Lemma rfd_iso : 'C_('Alt_T)[x | 'P] \isog 'Alt_T'.
diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v
index 0aacd7c..58c3cf0 100644
--- a/mathcomp/solvable/extraspecial.v
+++ b/mathcomp/solvable/extraspecial.v
@@ -420,7 +420,7 @@ have iC1U (U : {group gT}) x:
   by rewrite -norm_joinEl ?cardSg ?join_subG ?(subset_trans sUG).
 have oCG (U : {group gT}):
   Z \subset U -> U \subset G -> #|'C_G(U)| = (p * #|G : U|)%N.
-- elim: {U}_.+1 {-2}U (ltnSn #|U|) => // m IHm U leUm sZU sUG.
+- have [m] := ubnP #|U|; elim: m U => // m IHm U leUm sZU sUG.
   have [<- | neZU] := eqVneq Z U.
     by rewrite -oZ Lagrange // (setIidPl _) // centsC subsetIr.
   have{neZU} [x Gx not_cUx]: exists2 x, x \in G & x \notin 'C(U).
diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v
index be885b1..36c4d12 100644
--- a/mathcomp/solvable/extremal.v
+++ b/mathcomp/solvable/extremal.v
@@ -575,9 +575,9 @@ suffices{k k_gt0 le_k_n2} defGn2: <[x ^+ p]> \x <[y]> = 'Ohm_(n.-2)(G).
   rewrite -subSn // -subSS def_n1 def_n => -> /=; rewrite subnSK // subn2.
   by apply/eqP; rewrite eqEsubset OhmS ?Ohm_sub //= -{1}Ohm_id OhmS ?Ohm_leq.
 rewrite dprodEY //=; last by apply/trivgP; rewrite -tiXY setSI ?cycleX.
-apply/eqP; rewrite eqEsubset join_subG !cycle_subG /= {-2}(OhmE _ pG) -/r.
-rewrite def_n (subsetP (Ohm_leq G (ltn0Sn _))) // mem_gen /=; last first.
-  by rewrite !inE -order_dvdn oxp groupX /=.
+apply/eqP; rewrite eqEsubset join_subG !cycle_subG /= [in y \in _]def_n.
+rewrite (subsetP (Ohm_leq G (ltn0Sn _)) y) //= (OhmE _ pG) -/r.
+rewrite mem_gen /=; last by rewrite !inE -order_dvdn oxp groupX /=.
 rewrite gen_subG /= cent_joinEr // -defXY; apply/subsetP=> uv; case/setIP.
 case/imset2P=> u v Xu Yv ->{uv}; rewrite /r inE def_n expnS expgM.
 case/lcosetP: (XYp u v Xu Yv) => _ /cycleP[j ->] ->.
@@ -786,8 +786,8 @@ have defK: K = [set w].
   apply/eqP; rewrite eqEsubset sub1set Kw andbT subDset setUC.
   apply/subsetP=> uivj; have: uivj \in B by rewrite inE.
   rewrite -{1}defB => /imset2P[_ _ /cycleP[i ->] /cycleP[j ->] ->] {uivj}.
-  rewrite !inE sqrB -{-1}[j]odd_double_half.
-  case: (odd j); rewrite -order_dvdn ?ov // ou -def2r -mul2n dvdn_pmul2l //.
+  rewrite !inE sqrB; set b := odd j; rewrite -[j]odd_double_half -/b.
+  case: b; rewrite -order_dvdn ?ov // ou -def2r -mul2n dvdn_pmul2l //.
   case/dvdnP=> k ->{i}; apply/orP.
   rewrite add0n -[j./2]odd_double_half addnC doubleD -!muln2 -mulnA.
   rewrite -(expg_mod_order v) ov modnMDl; case: (odd _); last first.
diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v
index 28ca208..a96295f 100644
--- a/mathcomp/solvable/gseries.v
+++ b/mathcomp/solvable/gseries.v
@@ -116,7 +116,7 @@ Lemma subnormalP H G :
   reflect (exists2 s, normal.-series H s & last H s = G) (H <|<| G).
 Proof.
 apply: (iffP andP) => [[sHG snHG] | [s Hsn <-{G}]].
-  elim: {G}#|G| {-2}G sHG snHG => [|m IHm] G sHG.
+  move: #|G| snHG => m; elim: m => [|m IHm] in G sHG *.
     by exists [::]; last by apply/eqP; rewrite eq_sym.
   rewrite iterSr => /IHm[|s Hsn defG].
     by rewrite sub_gen // class_supportEr (bigD1 1) //= conjsg1 subsetUl.
@@ -125,10 +125,10 @@ apply: (iffP andP) => [[sHG snHG] | [s Hsn <-{G}]].
   by rewrite norms_gen ?class_support_norm.
 set f := fun _ => <<_>>; have idf: iter _ f H == H.
   by elim=> //= m IHm; rewrite (eqP IHm) /f class_support_id genGid.
-elim: {s}(size s) {-2}s (eqxx (size s)) Hsn => [[] //= | m IHm s].
-case/lastP: s => // s G; rewrite size_rcons last_rcons -cats1 cat_path /=.
-set K := last H s => def_m /and3P[Hsn /andP[sKG nKG] _].
-have:= sKG; rewrite subEproper; case/predU1P=> [<-|prKG]; first exact: IHm.
+have [m] := ubnP (size s); elim: m s Hsn => // m IHm /lastP[//|s G].
+rewrite size_rcons last_rcons rcons_path /= ltnS.
+set K := last H s => /andP[Hsn /andP[sKG nKG]] lt_s_m.
+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.
@@ -136,7 +136,8 @@ rewrite -(subnK (proper_card (sub_proper_trans sLK prKG))) iter_add 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.
-by rewrite {1 2}defH last_map (subset_trans sHK) //= (setIidPr sLK) => /eqP->.
+rewrite [in last _]defH last_map (subset_trans sHK) //=.
+by rewrite (setIidPr sLK) => /eqP->.
 Qed.
 
 Lemma subnormal_refl G : G <|<| G.
@@ -513,7 +514,7 @@ Qed.
 Lemma chief_series_exists H G :
   H <| G -> {s | (G.-chief).-series 1%G s & last 1%G s = H}.
 Proof.
-elim: {H}_.+1 {-2}H (ltnSn #|H|) => // m IHm U leUm nsUG.
+have [m] := ubnP #|H|; elim: m H => // m IHm U leUm nsUG.
 have [-> | ntU] := eqVneq U 1%G; first by exists [::].
 have [V maxV]: {V : {group gT} | maxnormal V U G}.
   by apply: ex_maxgroup; exists 1%G; rewrite proper1G ntU norms1.
diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v
index 43e429f..6234224 100644
--- a/mathcomp/solvable/hall.v
+++ b/mathcomp/solvable/hall.v
@@ -31,8 +31,8 @@ Implicit Type gT : finGroupType.
 Theorem SchurZassenhaus_split gT (G H : {group gT}) :
   Hall G H -> H <| G -> [splits G, over H].
 Proof.
-move: {2}_.+1 (ltnSn #|G|) => n; elim: n => // n IHn in gT G H *.
-rewrite ltnS => Gn hallH nsHG; have [sHG nHG] := andP nsHG.
+have [n] := ubnP #|G|; elim: n => // n IHn in gT G H * => /ltnSE-Gn hallH nsHG.
+have [sHG nHG] := andP nsHG.
 have [-> | [p pr_p pH]] := trivgVpdiv H.
   by apply/splitsP; exists G; rewrite inE -subG1 subsetIl mul1g eqxx.
 have [P sylP] := Sylow_exists p H.
@@ -102,8 +102,9 @@ Theorem SchurZassenhaus_trans_sol gT (H K K1 : {group gT}) :
     coprime #|H| #|K| -> #|K1| = #|K| ->
   exists2 x, x \in H & K1 :=: K :^ x.
 Proof.
-move: {2}_.+1 (ltnSn #|H|) => n; elim: n => // n IHn in gT H K K1 *.
-rewrite ltnS => leHn solH nHK; have [-> | ] := eqsVneq H 1.
+have [n] := ubnP #|H|.
+elim: n => // n IHn in gT H K K1 * => /ltnSE-leHn solH nHK.
+have [-> | ] := eqsVneq H 1.
   rewrite mul1g => sK1K _ eqK1K; exists 1; first exact: set11.
   by apply/eqP; rewrite conjsg1 eqEcard sK1K eqK1K /=.
 pose G := (H <*> K)%G.
@@ -150,9 +151,8 @@ Lemma SchurZassenhaus_trans_actsol gT (G A B : {group gT}) :
     coprime #|G| #|A| -> #|A| = #|B| ->
   exists2 x, x \in G & B :=: A :^ x.
 Proof.
-set AG := A <*> G; move: {2}_.+1 (ltnSn #|AG|) => n.
-elim: n => // n IHn in gT A B G AG *.
-rewrite ltnS => leAn solA nGA sB_AG coGA oAB.
+set AG := A <*> G; have [n] := ubnP #|AG|.
+elim: n => // n IHn in gT A B G AG * => /ltnSE-leAn solA nGA sB_AG coGA oAB.
 have [A1 | ntA] := eqsVneq A 1.
   by exists 1; rewrite // conjsg1 A1 (@card1_trivg _ B) // -oAB A1 cards1.
 have [M [sMA nsMA ntM]] := solvable_norm_abelem solA (normal_refl A) ntA.
@@ -218,8 +218,7 @@ Lemma Hall_exists_subJ pi gT (G : {group gT}) :
                 & forall K : {group gT}, K \subset G -> pi.-group K ->
                   exists2 x, x \in G & K \subset H :^ x.
 Proof.
-move: {2}_.+1 (ltnSn #|G|) => n.
-elim: n gT G => // n IHn gT G; rewrite ltnS => leGn solG.
+have [n] := ubnP #|G|; elim: n gT G => // n IHn gT G /ltnSE-leGn solG.
 have [-> | ntG] := eqsVneq G 1.
   exists 1%G => [|_ /trivGP-> _]; last by exists 1; rewrite ?set11 ?sub1G.
   by rewrite pHallE sub1G cards1 part_p'nat.
@@ -581,8 +580,8 @@ Proposition coprime_Hall_subset pi (gT : finGroupType) (A G X : {group gT}) :
     X \subset G -> pi.-group X -> A \subset 'N(X) ->
   exists H : {group gT}, [/\ pi.-Hall(G) H, A \subset 'N(H) & X \subset H].
 Proof.
-move: {2}_.+1 (ltnSn #|G|) => n.
-elim: n => // n IHn in gT A G X * => leGn nGA coGA solG sXG piX nXA.
+have [n] := ubnP #|G|.
+elim: n => // n IHn in gT A G X * => /ltnSE-leGn nGA coGA solG sXG piX nXA.
 have [G1 | ntG] := eqsVneq G 1.
   case: (coprime_Hall_exists pi nGA) => // H hallH nHA.
   by exists H; split; rewrite // (subset_trans sXG) // G1 sub1G.
diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v
index d191e20..3d3162b 100644
--- a/mathcomp/solvable/jordanholder.v
+++ b/mathcomp/solvable/jordanholder.v
@@ -174,8 +174,7 @@ Qed.
 Lemma JordanHolderUniqueness (G : gTg) (s1 s2 : seq gTg) :
   comps G s1 -> comps G s2 -> perm_eq (mkfactors G s1) (mkfactors G s2).
 Proof.
-elim: {G}#|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => cs1 cs2.
-  by rewrite leqNgt cardG_gt0 in cG.
+have [n] := ubnP #|G|; elim: n G => // n Hi G in s1 s2 * => /ltnSE-cG cs1 cs2.
 have [G1 | ntG] := boolP (G :==: 1).
   have -> : s1 = [::] by apply/eqP; rewrite -(trivg_comps cs1).
   have -> : s2 = [::] by apply/eqP; rewrite -(trivg_comps cs2).
@@ -188,10 +187,10 @@ case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}.
   by move: (trivg_comps cs2); rewrite eqxx; move/negP:ntG.
 case/andP: cs1 => /= lst1; case/andP=> maxN_1 pst1.
 case/andP: cs2 => /= lst2; case/andP=> maxN_2 pst2.
-have cN1 : #|N1| <= n.
-  by rewrite -ltnS (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_1).
-have cN2 : #|N2| <= n.
-  by rewrite -ltnS (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_2).
+have cN1 : #|N1| < n.
+  by rewrite (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_1).
+have cN2 : #|N2| < n.
+  by rewrite (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_2).
 case: (N1 =P N2) {s2 es2} => [eN12 |].
   by rewrite eN12 /= perm_cons Hi // /comps ?lst2 //= -eN12 lst1.
 move/eqP; rewrite -val_eqE /=; move/eqP=> neN12.
@@ -588,8 +587,7 @@ Lemma StrongJordanHolderUniqueness (G : {group rT}) (s1 s2 : seq {group rT}) :
     G \subset D -> acomps to G s1 -> acomps to G s2 -> 
   perm_eq (mkfactors G s1) (mkfactors G s2).
 Proof.
-elim: {G} #|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => hsD cs1 cs2.
-  by rewrite leqNgt cardG_gt0 in cG.
+have [n] := ubnP #|G|; elim: n G => // n Hi G in s1 s2 * => cG hsD cs1 cs2.
 case/orP: (orbN (G :==: 1)) => [tG | ntG].
   have -> : s1 = [::] by apply/eqP; rewrite -(trivg_acomps cs1).
   have -> : s2 = [::] by apply/eqP; rewrite -(trivg_acomps cs2).
@@ -608,10 +606,10 @@ have sN1D : N1 \subset D.
   by apply: subset_trans hsD; apply: maxainv_sub maxN_1.
 have sN2D : N2 \subset D.
   by apply: subset_trans hsD; apply: maxainv_sub maxN_2.
-have cN1 : #|N1| <= n.
-  by rewrite -ltnS (leq_trans _ cG) ?proper_card ?(maxainv_proper maxN_1).
-have cN2 : #|N2| <= n.
-  by rewrite -ltnS (leq_trans _ cG) ?proper_card ?(maxainv_proper maxN_2).
+have cN1 : #|N1| < n.
+  by rewrite -ltnS (leq_trans _ cG) ?ltnS ?proper_card ?(maxainv_proper maxN_1).
+have cN2 : #|N2| < n.
+  by rewrite -ltnS (leq_trans _ cG) ?ltnS ?proper_card ?(maxainv_proper maxN_2).
 case: (N1 =P N2) {s2 es2} => [eN12 |].
   by rewrite eN12 /= perm_cons Hi // /acomps ?lst2 //= -eN12 lst1.
 move/eqP; rewrite -val_eqE /=; move/eqP=> neN12.
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index 0dfb4d1..95b7184 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -993,7 +993,7 @@ Lemma card_subcent_extraspecial U :
   U \subset G -> #|'C_G(U)| = (#|'Z(G) :&: U| * #|G : U|)%N.
 Proof.
 move=> sUG; rewrite setIAC (setIidPr sUG).
-elim: {U}_.+1 {-2}U (ltnSn #|U|) sUG => // m IHm U leUm sUG.
+have [m leUm] := ubnP #|U|; elim: m => // m IHm in U leUm sUG *.
 have [cUG | not_cUG]:= orP (orbN (G \subset 'C(U))).
   by rewrite !(setIidPl _) ?Lagrange // centsC.
 have{not_cUG} [x Gx not_cUx] := subsetPn not_cUG.
@@ -1183,7 +1183,7 @@ Theorem extraspecial_structure S : p.-group S -> extraspecial S ->
   {Es | all (fun E => (#|E| == p ^ 3)%N && ('Z(E) == 'Z(S))) Es
       & \big[cprod/1%g]_(E <- Es) E \* 'Z(S) = S}.
 Proof.
-elim: {S}_.+1 {-2}S (ltnSn #|S|) => // m IHm S leSm pS esS.
+have [m] := ubnP #|S|; elim: m S => // m IHm S leSm pS esS.
 have [x Z'x]: {x | x \in S :\: 'Z(S)}.
   apply/sigW/set0Pn; rewrite -subset0 subDset setU0.
   apply: contra (extraspecial_nonabelian esS) => sSZ.
@@ -1210,11 +1210,11 @@ Let oZ := card_center_extraspecial pS esS.
 (* This is Aschbacher (23.10)(2). *)
 Lemma card_extraspecial : {n | n > 0 & #|S| = (p ^ n.*2.+1)%N}.
 Proof.
-exists (logn p #|S|)./2.
+set T := S; exists (logn p #|T|)./2.
   rewrite half_gt0 ltnW // -(leq_exp2l _ _ (prime_gt1 p_pr)) -card_pgroup //.
   exact: min_card_extraspecial.
-have [Es] := extraspecial_structure pS esS.
-elim: Es {3 4 5}S => [_ _ <-| E s IHs T] /=.
+have [Es] := extraspecial_structure pS esS; rewrite -[in RHS]/T.
+elim: Es T => [_ _ <-| E s IHs T] /=.
   by rewrite big_nil cprod1g oZ (pfactorK 1).
 rewrite -andbA big_cons -cprodA; case/and3P; move/eqP=> oEp3; move/eqP=> defZE.
 move/IHs=> {IHs}IHs; case/cprodP=> [[_ U _ defU]]; rewrite defU => defT cEU.
@@ -1233,8 +1233,8 @@ have [Es] := extraspecial_structure pS esS.
 elim: Es S oZ => [T _ _ <-| E s IHs T oZT] /=.
   rewrite big_nil cprod1g (center_idP (center_abelian T)).
   by apply/Aut_sub_fullP=> // g injg gZ; exists g.
-rewrite -andbA big_cons -cprodA; case/and3P; move/eqP=> oE; move/eqP=> defZE.
-move=> es_s; case/cprodP=> [[_ U _ defU]]; rewrite defU => defT cEU.
+rewrite -andbA big_cons -cprodA => /and3P[/eqP-oE /eqP-defZE es_s].
+case/cprodP=> -[_ U _ defU]; rewrite defU => defT cEU.
 have sUT: U \subset T by rewrite -defT mulG_subr.
 have sZU: 'Z(T) \subset U.
   by case/cprodP: defU => [[V _ -> _] <- _]; apply: mulG_subr.
diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v
index f0448d7..06f3152 100644
--- a/mathcomp/solvable/nilpotent.v
+++ b/mathcomp/solvable/nilpotent.v
@@ -238,8 +238,8 @@ apply/idP/mapP=> {s}/= [nilG | [n _ Ln1]]; last first.
   rewrite -subG1 {}Ln1; elim: n => // n IHn.
   by rewrite (subset_trans sHR) ?commSg.
 pose m := #|G|.-1; exists m; first by rewrite mem_iota /= prednK.
-rewrite ['L__(G)]card_le1_trivg //= -(subnn m).
-elim: {-2}m => [|n]; [by rewrite subn0 prednK | rewrite lcnSn subnS].
+set n := m; rewrite ['L__(G)]card_le1_trivg //= -(subnn m) -[m in _ - m]/n.
+elim: n => [|n]; [by rewrite subn0 prednK | rewrite lcnSn subnS].
 case: (eqsVneq 'L_n.+1(G) 1) => [-> | ntLn]; first by rewrite comm1G cards1.
 case: (m - n) => [|m' /= IHn]; first by rewrite leqNgt cardG_gt1 ntLn.
 rewrite -ltnS (leq_trans (proper_card _) IHn) //.
@@ -464,8 +464,8 @@ Qed.
 
 Lemma ucn_lcnP n G : ('L_n.+1(G) == 1) = ('Z_n(G) == G).
 Proof.
-rewrite !eqEsubset sub1G ucn_sub /= andbT -(ucn0 G).
-elim: {1 3}n 0 (addn0 n) => [j <- //|i IHi j].
+rewrite !eqEsubset sub1G ucn_sub /= andbT -(ucn0 G); set i := (n in LHS).
+have: i + 0 = n by [rewrite addn0]; elim: i 0 => [j <- //|i IHi j].
 rewrite addSnnS => /IHi <- {IHi}; rewrite ucnSn lcnSn.
 rewrite -sub_morphim_pre ?gFsub_trans ?gFnorm_trans // subsetI.
 by rewrite morphimS ?gFsub // quotient_cents2 ?gFsub_trans ?gFnorm_trans.
@@ -611,8 +611,8 @@ Qed.
 
 Lemma nilpotent_subnormal G H : nilpotent G -> H \subset G -> H <|<| G.
 Proof.
-move=> nilG; elim: {H}_.+1 {-2}H (ltnSn (#|G| - #|H|)) => // m IHm H.
-rewrite ltnS => leGHm sHG.
+move=> nilG; have [m] := ubnP (#|G| - #|H|).
+elim: m H => // m IHm H /ltnSE-leGHm sHG.
 have [->|] := eqVproper sHG; first exact: subnormal_refl.
 move/(nilpotent_proper_norm nilG); set K := 'N_G(H) => prHK.
 have snHK: H <|<| K by rewrite normal_subnormal ?normalSG.
diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v
index 5c572b7..2ed68f0 100644
--- a/mathcomp/solvable/pgroup.v
+++ b/mathcomp/solvable/pgroup.v
@@ -623,8 +623,8 @@ Proof. by rewrite /psubgroup sub1G pgroup1. Qed.
 
 Lemma Cauchy p G : prime p -> p %| #|G| -> {x | x \in G & #[x] = p}.
 Proof.
-move=> p_pr; elim: {G}_.+1 {-2}G (ltnSn #|G|) => // n IHn G.
-rewrite ltnS => leGn pG; pose xpG := [pred x in G | #[x] == p].
+move=> p_pr; have [n] := ubnP #|G|; elim: n G => // n IHn G /ltnSE-leGn pG.
+pose xpG := [pred x in G | #[x] == p].
 have [x /andP[Gx /eqP] | no_x] := pickP xpG; first by exists x.
 have{pG n leGn IHn} pZ: p %| #|'C_G(G)|.
   suffices /dvdn_addl <-:  p %| #|G :\: 'C(G)| by rewrite cardsID.
diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v
index 2a46564..f3ecae2 100644
--- a/mathcomp/solvable/sylow.v
+++ b/mathcomp/solvable/sylow.v
@@ -514,7 +514,7 @@ Qed.
 
 Lemma nil_Zgroup_cyclic G : Zgroup G -> nilpotent G -> cyclic G.
 Proof.
-elim: {G}_.+1 {-2}G (ltnSn #|G|) => // n IHn G; rewrite ltnS => leGn ZgG nilG.
+have [n] := ubnP #|G|; elim: n G => // n IHn G /ltnSE-leGn ZgG nilG.
 have [->|[p pr_p pG]] := trivgVpdiv G; first by rewrite -cycle1 cycle_cyclic.
 have /dprodP[_ defG Cpp' _] := nilpotent_pcoreC p nilG.
 have /cyclicP[x def_p]: cyclic 'O_p(G).
@@ -567,9 +567,8 @@ Theorem Baer_Suzuki x G :
     x \in G -> (forall y, y \in G -> p.-group <<[set x; x ^ y]>>) ->
   x \in 'O_p(G).
 Proof.
-elim: {G}_.+1 {-2}G x (ltnSn #|G|) => // n IHn G x; rewrite ltnS.
-set E := x ^: G => leGn Gx pE.
-have{pE} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}.
+have [n] := ubnP #|G|; elim: n G x => // n IHn G x /ltnSE-leGn Gx pE.
+set E := x ^: G; have{pE} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}.
   move=> _ _ /imsetP[y1 Gy1 ->] /imsetP[y2 Gy2 ->].
   rewrite -(mulgKV y1 y2) conjgM -2!conjg_set1 -conjUg genJ pgroupJ.
   by rewrite pE // groupMl ?groupV.