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.

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 :