3 files changed, 18 insertions, 18 deletions
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 9399035..ac785a3 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -2163,7 +2163,7 @@ case: (pickP (fun i : 'I_N => B ^+ i.+1 \subset B ^+ i)) => [n fixBn | no_fix].
   elim: {2}(n : nat) => [|m IHm]; first by rewrite mulg1.
   by apply: subset_trans fixBn; rewrite !expgSr mulgA mulSg.
 suffices: N < #|B ^+ N| by rewrite ltnNge max_card.
-elim: {-2}N (leqnn N) => [|n IHn] lt_nN; first by rewrite cards1.
+have [] := ubnPgeq N; elim=> [|n IHn] lt_nN; first by rewrite cards1.
 apply: leq_ltn_trans (IHn (ltnW lt_nN)) (proper_card _).
 by rewrite /proper (no_fix (Ordinal lt_nN)) expgS mulUg mul1g subsetUl.
 Qed.
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index 853ffb6..8357bc4 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -591,8 +591,8 @@ Proof.
 apply: (iffP eqP) => [defG i j Pi Pj neq_ij | cHH].
   rewrite (bigD1 j) // (bigD1 i) /= ?cprodA in defG; last exact/andP.
   by case/cprodP: defG => [[K _ /cprodP[//]]].
-set Q := P; have: subpred Q P by [].
-elim: {Q}_.+1 {-2}Q (ltnSn #|Q|) => // n IHn Q leQn sQP.
+set Q := P; have sQP: subpred Q P by []; have [n leQn] := ubnP #|Q|.
+elim: n => // n IHn in (Q) leQn sQP *.
 have [i Qi | Q0] := pickP Q; last by rewrite !big_pred0.
 rewrite (cardD1x Qi) add1n ltnS !(bigD1 i Qi) /= in leQn *.
 rewrite {}IHn {n leQn}// => [|j /andP[/sQP //]].
@@ -620,7 +620,7 @@ transitivity (\prod_(j <- rot n r2) x j).
   rewrite Dr2 !big_cons in defG Ax *; have [[_ G1 _ defG1] _ _] := cprodP defG.
   rewrite (IHr r3 G1) //; first by case/allP/andP: Ax => _ /allP.
   by rewrite -(perm_cons i) -Dr2 perm_sym perm_rot perm_sym.
-rewrite -{-2}(cat_take_drop n r2) in eq_r12 *.
+rewrite -(cat_take_drop n r2) [in LHS]cat_take_drop in eq_r12 *.
 rewrite (perm_big _ eq_r12) !big_cat /= !(big_nth i) !big_mkord in defG *.
 have /cprodP[[G1 G2 defG1 defG2] _ /centsP-> //] := defG.
   rewrite defG2 -(bigcprodW defG2) mem_prodg // => k _; apply: Ax.
@@ -763,8 +763,8 @@ Proof.
 apply: (iffP eqP) => [defG i Pi | dxG].
   rewrite !(bigD1 i Pi) /= in defG; have [[_ G' _ defG'] _ _ _] := dprodP defG.
   by apply/dprodYP; rewrite -defG defG' bigprodGE (bigdprodWY defG').
-set Q := P; have: subpred Q P by [].
-elim: {Q}_.+1 {-2}Q (ltnSn #|Q|) => // n IHn Q leQn sQP.
+set Q := P; have sQP: subpred Q P by []; have [n leQn] := ubnP #|Q|.
+elim: n => // n IHn in (Q) leQn sQP *.
 have [i Qi | Q0] := pickP Q; last by rewrite !big_pred0.
 rewrite (cardD1x Qi) add1n ltnS !(bigD1 i Qi) /= in leQn *.
 rewrite {}IHn {n leQn}// => [|j /andP[/sQP //]].
@@ -820,8 +820,8 @@ Lemma bigcprod_coprime_dprod (I : finType) (P : pred I) (A : I -> {set gT}) G :
     (forall i j, P i -> P j -> i != j -> coprime #|A i| #|A j|) ->
   \big[dprod/1]_(i | P i) A i = G.
 Proof.
-move=> defG coA; set Q := P in defG *; have: subpred Q P by [].
-elim: {Q}_.+1 {-2}Q (ltnSn #|Q|) => // m IHm Q leQm in G defG * => sQP.
+move=> defG coA; set Q := P in defG *; have sQP: subpred Q P by [].
+have [m leQm] := ubnP #|Q|; elim: m => // m IHm in (Q) leQm G defG sQP *.
 have [i Qi | Q0] := pickP Q; last by rewrite !big_pred0 in defG *.
 move: defG; rewrite !(bigD1 i Qi) /= => /cprodP[[Hi Gi defAi defGi] <-].
 rewrite defAi defGi => cHGi.
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index f1ff532..b35ab1d 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -465,18 +465,18 @@ Arguments dpair {eT}.
 Lemma prod_tpermP s :
   {ts : seq (T * T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}.
 Proof.
-elim: {s}_.+1 {-2}s (ltnSn #|[pred x | s x != x]|) => // n IHn s.
-rewrite ltnS => le_s_n; case: (pickP (fun x => s x != x)) => [x s_x | s_id].
-  have [|ts def_s ne_ts] := IHn (tperm x (s^-1 x) * s).
-    rewrite (cardD1 x) !inE s_x in le_s_n; apply: leq_ltn_trans le_s_n.
-    apply: subset_leq_card; apply/subsetP=> y.
-    rewrite !inE permM permE /= -(canF_eq (permK _)).
-    have [-> | ne_yx] := altP (y =P x); first by rewrite permKV eqxx.
-    by case: (s y =P x) => // -> _; rewrite eq_sym.
+have [n] := ubnP #|[pred x | s x != x]|; elim: n s => // n IHn s /ltnSE-le_s_n.
+case: (pickP (fun x => s x != x)) => [x s_x | s_id]; last first.
+  exists nil; rewrite // big_nil; apply/permP=> x.
+  by apply/eqP/idPn; rewrite perm1 s_id.
+have [|ts def_s ne_ts] := IHn (tperm x (s^-1 x) * s); last first.
   exists ((x, s^-1 x) :: ts); last by rewrite /= -(canF_eq (permK _)) s_x.
   by rewrite big_cons -def_s mulgA tperm2 mul1g.
-exists nil; rewrite // big_nil; apply/permP=> x.
-by apply/eqP/idPn; rewrite perm1 s_id.
+rewrite (cardD1 x) !inE s_x in le_s_n; apply: leq_ltn_trans le_s_n.
+apply: subset_leq_card; apply/subsetP=> y.
+rewrite !inE permM permE /= -(canF_eq (permK _)).
+have [-> | ne_yx] := altP (y =P x); first by rewrite permKV eqxx.
+by case: (s y =P x) => // -> _; rewrite eq_sym.
 Qed.
 
 Lemma odd_perm_prod ts :