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.

8 files changed, 163 insertions, 122 deletions

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index adb4094..f596c3f 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1392,10 +1392,10 @@ Lemma partition_big (I J : finType) (P : pred I) p (Q : pred J) F :
 Proof.
 move=> Qp; transitivity (\big[*%M/1]_(i | P i && Q (p i)) F i).
   by apply: eq_bigl => i; case Pi: (P i); rewrite // Qp.
-elim: {Q Qp}_.+1 {-2}Q (ltnSn #|Q|) => // n IHn Q.
-case: (pickP Q) => [j Qj | Q0 _]; last first.
+have [n leQn] := ubnP #|Q|; elim: n => // n IHn in Q {Qp} leQn *.
+case: (pickP Q) => [j Qj | Q0]; last first.
   by rewrite !big_pred0 // => i; rewrite Q0 andbF.
-rewrite ltnS (cardD1x j Qj) (bigD1 j) //; move/IHn=> {n IHn} <-.
+rewrite (bigD1 j) // -IHn; last by rewrite ltnS (cardD1x j Qj) in leQn.
 rewrite (bigID (fun i => p i == j)); congr (_ * _); apply: eq_bigl => i.
   by case: eqP => [-> | _]; rewrite !(Qj, simpm).
 by rewrite andbA.
@@ -1408,14 +1408,13 @@ Lemma reindex_onto (I J : finType) (h : J -> I) h' (P : pred I) F :
   \big[*%M/1]_(i | P i) F i =
     \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j).
 Proof.
-move=> h'K; elim: {P}_.+1 {-3}P h'K (ltnSn #|P|) => //= n IHn P h'K.
-case: (pickP P) => [i Pi | P0 _]; last first.
+move=> h'K; have [n lePn] := ubnP #|P|; elim: n => // n IHn in P h'K lePn *.
+case: (pickP P) => [i Pi | P0]; last first.
   by rewrite !big_pred0 // => j; rewrite P0.
-rewrite ltnS (cardD1x i Pi); move/IHn {n IHn} => IH.
 rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eq_refl //=; congr (_ * _).
-rewrite {}IH => [|j]; [apply: eq_bigl => j | by case/andP; auto].
-rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK; congr (_ && ~~ _).
-by apply/eqP/eqP=> [<-|->] //; rewrite h'K.
+rewrite {}IHn => [|j /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. 
+apply: eq_bigl => j; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK.
+by congr (_ && ~~ _); apply/eqP/eqP=> [<-|->] //; rewrite h'K.
 Qed.
 Arguments reindex_onto [I J] h h' [P F].
 
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index 0c5be52..8bdb426 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -508,13 +508,13 @@ suffices [le_i_ti le_ti_ni]: i <= tnth t i /\ tnth t i <= i + n.
   by rewrite /sub_mn inordK ?subnKC // ltnS leq_subLR.
 pose y0 := tnth t i; rewrite (tnth_nth y0) -(nth_map _ (val i)) ?size_tuple //.
 case def_e: (map _ _) => [|x e] /=; first by rewrite nth_nil ?leq_addr.
-rewrite def_e in inc_t; split.
-  case: {-2}i; rewrite /= -{1}(size_tuple t) -(size_map val) def_e.
-  elim=> //= j IHj lt_j_t; apply: leq_trans (pathP (val i) inc_t _ lt_j_t).
-  by rewrite ltnS IHj 1?ltnW.
+set nth_i := nth (i : nat); rewrite def_e in inc_t; split.
+  have: i < size (x :: e) by rewrite -def_e size_map size_tuple ltn_ord.
+  elim: (val i) => //= j IHj lt_j_e.
+  by apply: leq_trans (pathP (val i) inc_t _ lt_j_e); rewrite ltnS IHj 1?ltnW.
 move: (_ - _) (subnK (valP i)) => k /=.
-elim: k {-2}(val i) => /= [|k IHk] j def_m; rewrite -ltnS -addSn.
-  by rewrite [j.+1]def_m -def_e (nth_map y0) ?ltn_ord // size_tuple -def_m.
+elim: k (val i) => /= [|k IHk] j; rewrite -ltnS -addSn ?add0n => def_m.
+  by rewrite def_m -def_e /nth_i (nth_map y0) ?ltn_ord // size_tuple -def_m.
 rewrite (leq_trans _ (IHk _ _)) -1?addSnnS //; apply: (pathP _ inc_t).
 rewrite -ltnS (leq_trans (leq_addl k _)) // -addSnnS def_m.
 by rewrite -(size_tuple t) -(size_map val) def_e.
diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v
index 49d50fe..4d7843c 100644
--- a/mathcomp/ssreflect/choice.v
+++ b/mathcomp/ssreflect/choice.v
@@ -90,11 +90,12 @@ Qed.
 Lemma codeK : cancel code decode.
 Proof.
 elim=> //= v s IHs; rewrite -[_ * _]prednK ?muln_gt0 ?expn_gt0 //=.
-rewrite -{3}[v]addn0; elim: v {1 4}0 => [|v IHv {IHs}] q.
-  rewrite mul1n /= -{1}addnn -{4}IHs; move: (_ s) {IHs} => n.
-  by elim: {1 3}n => //=; case: n.
+set two := 2; rewrite -[v in RHS]addn0; elim: v 0 => [|v IHv {IHs}] q.
+  rewrite mul1n add0n /= -{}[in RHS]IHs; case: (code s) => // u; pose n := u.+1.
+  by transitivity [rec q, n + u.+1, n.*2]; [rewrite addnn | elim: n => //=].
 rewrite expnS -mulnA mul2n -{1}addnn -[_ * _]prednK ?muln_gt0 ?expn_gt0 //.
-by rewrite doubleS addSn /= addSnnS; elim: {-2}_.-1 => //=.
+set u := _.-1 in IHv *; set n := u; rewrite [in u1 in _ + u1]/n.
+by rewrite [in RHS]addSnnS -{}IHv; elim: n.
 Qed.
 
 Lemma ltn_code s : all (fun j => j < code s) s.
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 48fb9fb..06a6ff1 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -40,11 +40,10 @@ Variant edivn_spec m d : nat * nat -> Type :=
 
 Lemma edivnP m d : edivn_spec m d (edivn m d).
 Proof.
-rewrite -{1}[m]/(0 * d + m) /edivn; case: d => //= d.
-elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //= le_mn.
-have le_m'n: m - d <= n by rewrite (leq_trans (leq_subr d m)).
-rewrite subn_if_gt; case: ltnP => [// | le_dm].
-by rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn.
+rewrite -[m in edivn_spec m]/(0 * d + m) /edivn; case: d => //= d.
+elim/ltn_ind: m 0 => -[|m] IHm q //=; rewrite subn_if_gt.
+case: ltnP => // le_dm; rewrite -[in m.+1](subnKC le_dm) -addSn.
+by rewrite addnA -mulSnr; apply/IHm/leq_subr.
 Qed.
 
 Lemma edivn_eq d q r : r < d -> edivn (q * d + r) d = (q, r).
@@ -75,10 +74,8 @@ Notation "m != n %[mod d ]" := (m %% d != n %% d) : nat_scope.
 
 Lemma modn_def m d : m %% d = (edivn m d).2.
 Proof.
-case: d => //= d; rewrite /modn /edivn /=.
-elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=.
-rewrite ltnS !subn_if_gt; case: (d <= m) => // le_mn.
-by apply: IHn; apply: leq_trans le_mn; apply: leq_subr.
+case: d => //= d; rewrite /modn /edivn /=; elim/ltn_ind: m 0 => -[|m] IHm q //=.
+by rewrite !subn_if_gt; case: (d <= m) => //; apply/IHm/leq_subr.
 Qed.
 
 Lemma edivn_def m d : edivn m d = (m %/ d, m %% d).
@@ -97,7 +94,7 @@ Proof. by move=> lt_md; rewrite /divn (edivn_eq 0). Qed.
 
 Lemma divnMDl q m d : 0 < d -> (q * d + m) %/ d = q + m %/ d.
 Proof.
-move=> d_gt0; rewrite {1}(divn_eq m d) addnA -mulnDl.
+move=> d_gt0; rewrite [in LHS](divn_eq m d) addnA -mulnDl.
 by rewrite /divn edivn_eq // modn_def; case: edivnP; rewrite d_gt0.
 Qed.
 
@@ -109,22 +106,22 @@ Proof. by move=> d_gt0; rewrite mulnC mulnK. Qed.
 
 Lemma expnB p m n : p > 0 -> m >= n -> p ^ (m - n) = p ^ m %/ p ^ n.
 Proof.
-by move=> p_gt0 /subnK{2}<-; rewrite expnD mulnK // expn_gt0 p_gt0.
+by move=> p_gt0 /subnK-Dm; rewrite -[in RHS]Dm expnD mulnK // expn_gt0 p_gt0.
 Qed.
 
 Lemma modn1 m : m %% 1 = 0.
 Proof. by rewrite modn_def; case: edivnP => ? []. Qed.
 
 Lemma divn1 m : m %/ 1 = m.
-Proof. by rewrite {2}(@divn_eq m 1) // modn1 addn0 muln1. Qed.
+Proof. by rewrite [RHS](@divn_eq m 1) // modn1 addn0 muln1. Qed.
 
 Lemma divnn d : d %/ d = (0 < d).
-Proof. by case: d => // d; rewrite -{1}[d.+1]muln1 mulKn. Qed.
+Proof. by case: d => // d; rewrite -[n in n %/ _]muln1 mulKn. Qed.
 
 Lemma divnMl p m d : p > 0 -> p * m %/ (p * d) = m %/ d.
 Proof.
 move=> p_gt0; case: (posnP d) => [-> | d_gt0]; first by rewrite muln0.
-rewrite {2}/divn; case: edivnP; rewrite d_gt0 /= => q r ->{m} lt_rd.
+rewrite [RHS]/divn; case: edivnP; rewrite d_gt0 /= => q r ->{m} lt_rd.
 rewrite mulnDr mulnCA divnMDl; last by rewrite muln_gt0 p_gt0.
 by rewrite addnC divn_small // ltn_pmul2l.
 Qed.
@@ -141,10 +138,10 @@ Lemma ltn_pmod m d : 0 < d -> m %% d < d.
 Proof. by rewrite ltn_mod. Qed.
 
 Lemma leq_trunc_div m d : m %/ d * d <= m.
-Proof. by rewrite {2}(divn_eq m d) leq_addr. Qed.
+Proof. by rewrite [m in _ <= m](divn_eq m d) leq_addr. Qed.
 
 Lemma leq_mod m d : m %% d  <= m.
-Proof. by rewrite {2}(divn_eq m d) leq_addl. Qed.
+Proof. by rewrite [m in _ <= m](divn_eq m d) leq_addl. Qed.
 
 Lemma leq_div m d : m %/ d <= m.
 Proof.
@@ -153,7 +150,7 @@ Qed.
 
 Lemma ltn_ceil m d : 0 < d -> m < (m %/ d).+1 * d.
 Proof.
-by move=> d_gt0; rewrite {1}(divn_eq m d) -addnS mulSnr leq_add2l ltn_mod.
+by move=> d_gt0; rewrite [in m.+1](divn_eq m d) -addnS mulSnr leq_add2l ltn_mod.
 Qed.
 
 Lemma ltn_divLR m n d : d > 0 -> (m %/ d < n) = (m < n * d).
@@ -244,7 +241,7 @@ Qed.
 Lemma divnMA m n p : m %/ (n * p) = m %/ n %/ p.
 Proof.
 case: n p => [|n] [|p]; rewrite ?muln0 ?div0n //.
-rewrite {2}(divn_eq m (n.+1 * p.+1)) mulnA mulnAC !divnMDl //.
+rewrite [in RHS](divn_eq m (n.+1 * p.+1)) mulnA mulnAC !divnMDl //.
 by rewrite [_ %/ p.+1]divn_small ?addn0 // ltn_divLR // mulnC ltn_mod.
 Qed.
 
@@ -252,7 +249,7 @@ Lemma divnAC m n p : m %/ n %/ p =  m %/ p %/ n.
 Proof. by rewrite -!divnMA mulnC. Qed.
 
 Lemma modn_small m d : m < d -> m %% d = m.
-Proof. by move=> lt_md; rewrite {2}(divn_eq m d) divn_small. Qed.
+Proof. by move=> lt_md; rewrite [RHS](divn_eq m d) divn_small. Qed.
 
 Lemma modn_mod m d : m %% d = m %[mod d].
 Proof. by case: d => // d; apply: modn_small; rewrite ltn_mod. Qed.
@@ -287,7 +284,7 @@ Lemma modnDr m d : m + d = m %[mod d].
 Proof. by rewrite addnC modnDl. Qed.
 
 Lemma modnn d : d %% d = 0.
-Proof. by rewrite -{1}[d]addn0 modnDl mod0n. Qed.
+Proof. by rewrite -[d in d %% _]addn0 modnDl mod0n. Qed.
 
 Lemma modnMl p d : p * d %% d = 0.
 Proof. by rewrite -[p * d]addn0 modnMDl mod0n. Qed.
@@ -296,7 +293,7 @@ Lemma modnMr p d : d * p %% d = 0.
 Proof. by rewrite mulnC modnMl. Qed.
 
 Lemma modnDml m n d : m %% d + n = m + n %[mod d].
-Proof. by rewrite {2}(divn_eq m d) -addnA modnMDl. Qed.
+Proof. by rewrite [in RHS](divn_eq m d) -addnA modnMDl. Qed.
 
 Lemma modnDmr m n d : m + n %% d = m + n %[mod d].
 Proof. by rewrite !(addnC m) modnDml. Qed.
@@ -316,7 +313,7 @@ Lemma eqn_modDr p m n d : (m + p == n + p %[mod d]) = (m == n %[mod d]).
 Proof. by rewrite -!(addnC p) eqn_modDl. Qed.
 
 Lemma modnMml m n d : m %% d * n = m * n %[mod d].
-Proof. by rewrite {2}(divn_eq m d) mulnDl mulnAC modnMDl. Qed.
+Proof. by rewrite [in RHS](divn_eq m d) mulnDl mulnAC modnMDl. Qed.
 
 Lemma modnMmr m n d : m * (n %% d) = m * n %[mod d].
 Proof. by rewrite !(mulnC m) modnMml. Qed.
@@ -328,11 +325,11 @@ Lemma modn2 m : m %% 2 = odd m.
 Proof. by elim: m => //= m IHm; rewrite -addn1 -modnDml IHm; case odd. Qed.
 
 Lemma divn2 m : m %/ 2 = m./2.
-Proof. by rewrite {2}(divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed.
+Proof. by rewrite [in RHS](divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed.
 
 Lemma odd_mod m d : odd d = false -> odd (m %% d) = odd m.
 Proof.
-by move=> d_even; rewrite {2}(divn_eq m d) odd_add odd_mul d_even andbF.
+by move=> d_even; rewrite [in RHS](divn_eq m d) odd_add odd_mul d_even andbF.
 Qed.
 
 Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n].
@@ -349,7 +346,7 @@ Notation "m %| d" := (dvdn m d) : nat_scope.
 Lemma dvdnP d m : reflect (exists k, m = k * d) (d %| m).
 Proof.
 apply: (iffP eqP) => [md0 | [k ->]]; last by rewrite modnMl.
-by exists (m %/ d); rewrite {1}(divn_eq m d) md0 addn0.
+by exists (m %/ d); rewrite [LHS](divn_eq m d) md0 addn0.
 Qed.
 Arguments dvdnP {d m}.
 
@@ -389,7 +386,7 @@ Proof. by move=> d_dv_n /dvdnP[n1 ->]; apply: dvdn_mull. Qed.
 Lemma dvdn_eq d m : (d %| m) = (m %/ d * d == m).
 Proof.
 apply/eqP/eqP=> [modm0 | <-]; last exact: modnMl.
-by rewrite {2}(divn_eq m d) modm0 addn0.
+by rewrite [RHS](divn_eq m d) modm0 addn0.
 Qed.
 
 Lemma dvdn2 n : (2 %| n) = ~~ odd n.
@@ -428,11 +425,11 @@ Lemma muln_divCA d m n : d %| m -> d %| n -> m * (n %/ d) = n * (m %/ d).
 Proof. by move=> dv_d_m dv_d_n; rewrite mulnC divn_mulAC ?muln_divA. Qed.
 
 Lemma divnA m n p : p %| n -> m %/ (n %/ p) = m * p %/ n.
-Proof. by case: p => [|p] dv_n; rewrite -{2}(divnK dv_n) // divnMr. Qed.
+Proof. by case: p => [|p] dv_n; rewrite -[in RHS](divnK dv_n) // divnMr. Qed.
 
 Lemma modn_dvdm m n d : d %| m -> n %% m = n %[mod d].
 Proof.
-by case/dvdnP=> q def_m; rewrite {2}(divn_eq n m) {3}def_m mulnA modnMDl.
+by case/dvdnP=> q def_m; rewrite [in RHS](divn_eq n m) def_m mulnA modnMDl.
 Qed.
 
 Lemma dvdn_leq d m : 0 < m -> d %| m -> d <= m.
@@ -518,7 +515,7 @@ Hint Resolve dvdn_add dvdn_sub dvdn_exp : core.
 
 Lemma eqn_mod_dvd d m n : n <= m -> (m == n %[mod d]) = (d %| m - n).
 Proof.
-by move=> le_mn; rewrite -{1}[n]add0n -{1}(subnK le_mn) eqn_modDr mod0n.
+by move/subnK=> Dm; rewrite -[n in LHS]add0n -[in LHS]Dm eqn_modDr mod0n.
 Qed.
 
 Lemma divnDMl q m d : 0 < d -> (m + q * d) %/ d = (m %/ d) + q.
@@ -531,16 +528,16 @@ Lemma divnBMl q m d : (m - q * d) %/ d = (m %/ d) - q.
 Proof. by case: d => [|d]//=; rewrite divnB// mulnK// modnMl ltn0 subn0. Qed.
 
 Lemma divnDl m n d : d %| m -> (m + n) %/ d = m %/ d + n %/ d.
-Proof. by case: d => // d /divnK{1}<-; rewrite divnMDl. Qed.
+Proof. by case: d => // d /divnK-Dm; rewrite -[in LHS]Dm divnMDl. Qed.
 
 Lemma divnDr m n d : d %| n -> (m + n) %/ d = m %/ d + n %/ d.
 Proof. by move=> dv_n; rewrite addnC divnDl // addnC. Qed.
 
 Lemma divnBl m n d : d %| m -> (m - n) %/ d = m %/ d - (n %/ d) - (~~ (d %| n)).
-Proof. by case: d => [|d] // /divnK {1}<-; rewrite divnMBl. Qed.
+Proof. by case: d => [|d] // /divnK-Dm; rewrite -[in LHS]Dm divnMBl. Qed.
 
 Lemma divnBr m n d : d %| n -> (m - n) %/ d = m %/ d - n %/ d.
-Proof. by case: d => [|d]// /divnK {1}<-; rewrite divnBMl. Qed.
+Proof. by case: d => [|d]// /divnK-Dm; rewrite -[in LHS]Dm divnBMl. Qed.
 
 Lemma edivnS m d : 0 < d -> edivn m.+1 d =
   if d %| m.+1 then ((m %/ d).+1, 0) else (m %/ d, (m %% d).+1).
@@ -592,11 +589,11 @@ Definition gcdn := nosimpl gcdn_rec.
 
 Lemma gcdnE m n : gcdn m n = if m == 0 then n else gcdn (n %% m) m.
 Proof.
-rewrite /gcdn; elim: m {-2}m (leqnn m) n => [|s IHs] [|m] le_ms [|n] //=.
-case def_n': (_ %% _) => // [n'].
-have{def_n'} lt_n'm: n' < m by rewrite -def_n' -ltnS ltn_pmod.
-rewrite {}IHs ?(leq_trans lt_n'm) // subn_if_gt ltnW //=; congr gcdn_rec.
-by rewrite -{2}(subnK (ltnW lt_n'm)) -addnS modnDr.
+rewrite /gcdn; elim/ltn_ind: m n => -[|m] IHm [|n] //=.
+case def_p: (_ %% _) => // [p].
+have{def_p} lt_pm: p.+1 < m.+1 by rewrite -def_p ltn_pmod.
+rewrite {}IHm // subn_if_gt ltnW //=; congr gcdn_rec.
+by rewrite -(subnK (ltnW lt_pm)) modnDr.
 Qed.
 
 Lemma gcdnn : idempotent gcdn.
@@ -606,7 +603,7 @@ Lemma gcdnC : commutative gcdn.
 Proof.
 move=> m n; wlog lt_nm: m n / n < m.
   by case: (ltngtP n m) => [||-> //]; last symmetry; auto.
-by rewrite gcdnE -{1}(ltn_predK lt_nm) modn_small.
+by rewrite gcdnE -[in m == 0](ltn_predK lt_nm) modn_small.
 Qed.
 
 Lemma gcd0n : left_id 0 gcdn. Proof. by case. Qed.
@@ -620,11 +617,11 @@ Proof. by move=> n; rewrite gcdnC gcd1n. Qed.
 
 Lemma dvdn_gcdr m n : gcdn m n %| n.
 Proof.
-elim: m {-2}m (leqnn m) n => [|s IHs] [|m] le_ms [|n] //.
-rewrite gcdnE; case def_n': (_ %% _) => [|n']; first by rewrite /dvdn def_n'.
-have lt_n's: n' < s by rewrite -ltnS (leq_trans _ le_ms) // -def_n' ltn_pmod.
-rewrite /= (divn_eq n.+1 m.+1) def_n' dvdn_addr ?dvdn_mull //; last exact: IHs.
-by rewrite gcdnE /= IHs // (leq_trans _ lt_n's) // ltnW // ltn_pmod.
+elim/ltn_ind: m n => -[|m] IHm [|n] //=.
+rewrite gcdnE; case def_p: (_ %% _) => [|p]; first by rewrite /dvdn def_p.
+have lt_pm: p < m by rewrite -ltnS -def_p ltn_pmod.
+rewrite /= (divn_eq n.+1 m.+1) def_p dvdn_addr ?dvdn_mull //; last exact: IHm.
+by rewrite gcdnE /= IHm // (ltn_trans (ltn_pmod _ _)). 
 Qed.
 
 Lemma dvdn_gcdl m n : gcdn m n %| m.
@@ -639,7 +636,7 @@ Lemma gcdnMDl k m n : gcdn m (k * m + n) = gcdn m n.
 Proof. by rewrite !(gcdnE m) modnMDl mulnC; case: m. Qed.
 
 Lemma gcdnDl m n : gcdn m (m + n) = gcdn m n.
-Proof. by rewrite -{2}(mul1n m) gcdnMDl. Qed.
+Proof. by rewrite -[m in m + n]mul1n gcdnMDl. Qed.
 
 Lemma gcdnDr m n : gcdn m (n + m) = gcdn m n.
 Proof. by rewrite addnC gcdnDl. Qed.
@@ -665,7 +662,7 @@ rewrite /minn; case: leqP; [rewrite gcdnC | move/ltnW];
 Qed.
 
 Lemma gcdn_modr m n : gcdn m (n %% m) = gcdn m n.
-Proof. by rewrite {2}(divn_eq n m) gcdnMDl. Qed.
+Proof. by rewrite [in RHS](divn_eq n m) gcdnMDl. Qed.
 
 Lemma gcdn_modl m n : gcdn (m %% n) n = gcdn m n.
 Proof. by rewrite !(gcdnC _ n) gcdn_modr. Qed.
@@ -694,16 +691,16 @@ Proof. by case: n. Qed.
 
 Lemma egcdnP m n : m > 0 -> egcdn_spec m n (egcdn m n).
 Proof.
-rewrite /egcdn; have: (n, m) = Bezout_rec n m [::] by [].
-case: (posnP n) => [-> /=|]; first by split; rewrite // mul1n gcdn0.
-move: {2 6}n {4 6}n {1 4}m [::] (ltnSn n) => s n0 m0.
-elim: s n m => [[]//|s IHs] n m qs /= le_ns n_gt0 def_mn0 m_gt0.
-case: edivnP => q r def_m; rewrite n_gt0 /= => lt_rn.
-case: posnP => [r0 {s le_ns IHs lt_rn}|r_gt0]; last first.
-  by apply: IHs => //=; [rewrite (leq_trans lt_rn) | rewrite natTrecE -def_m].
+have [-> /= | n_gt0 m_gt0] := posnP n; first by split; rewrite // mul1n gcdn0.
+rewrite /egcdn; set s := (s in egcdn_rec _ _ s); pose bz := Bezout_rec n m [::].
+have: n < s.+1 by []; move defSpec: (egcdn_spec bz.2 bz.1) s => Spec s.
+elim: s => [[]|s IHs] //= in n m (qs := [::]) bz defSpec n_gt0 m_gt0 *.
+case: edivnP => q r def_m; rewrite n_gt0 ltnS /= => lt_rn le_ns1.
+case: posnP => [r0 {s le_ns1 IHs lt_rn}|r_gt0]; last first.
+  by apply: IHs => //=; [rewrite natTrecE -def_m | rewrite (leq_trans lt_rn)].
 rewrite {r}r0 addn0 in def_m; set b := odd _; pose d := gcdn m n.
 pose km := ~~ b : nat; pose kn := if b then 1 else q.-1.
-rewrite (_ : Bezout_rec _ _ _ = Bezout_rec km kn qs); last first.
+rewrite [bz in Spec bz](_ : _ = Bezout_rec km kn qs); last first.
   by rewrite /kn /km; case: (b) => //=; rewrite natTrecE addn0 muln1.
 have def_d: d = n by rewrite /d def_m gcdnC gcdnE modnMl gcd0n -[n]prednK.
 have: km * m + 2 * b * d = kn * n + d.
@@ -713,14 +710,13 @@ have{def_m}: kn * d <= m.
   have q_gt0 : 0 < q by rewrite def_m muln_gt0 n_gt0 ?andbT in m_gt0.
   by rewrite /kn; case b; rewrite def_d def_m leq_pmul2r // leq_pred.
 have{def_d}: km * d <= n by rewrite -[n]mul1n def_d leq_pmul2r // leq_b1.
-move: km {q}kn m_gt0 n_gt0 def_mn0; rewrite {}/d {}/b.
+move: km {q}kn m_gt0 n_gt0 defSpec; rewrite {}/b {}/d {}/bz.
 elim: qs m n => [|q qs IHq] n r kn kr n_gt0 r_gt0 /=.
-  case=> -> -> {m0 n0}; rewrite !addn0 => le_kn_r _ def_d; split=> //.
-  have d_gt0: 0 < gcdn n r by rewrite gcdn_gt0 n_gt0.
-  have: 0 < kn * n by rewrite def_d addn_gt0 d_gt0 orbT.
-  rewrite muln_gt0 n_gt0 andbT; move/ltn_pmul2l <-.
+  set d := gcdn n r; rewrite mul0n addn0 => <- le_kn_r _ def_d; split=> //.
+  have d_gt0: 0 < d by rewrite gcdn_gt0 n_gt0.
+  have /ltn_pmul2l<-: 0 < kn by rewrite -(ltn_pmul2r n_gt0) def_d ltn_addl.
   by rewrite def_d -addn1 leq_add // mulnCA leq_mul2l le_kn_r orbT.
-rewrite !natTrecE; set m:= _ + r; set km := _ * _ + kn; pose d := gcdn m n.
+rewrite !natTrecE; set m := _ + r; set km := _ + kn; pose d := gcdn m n.
 have ->: gcdn n r = d by rewrite [d]gcdnC gcdnMDl.
 have m_gt0: 0 < m by rewrite addn_gt0 r_gt0 orbT.
 have d_gt0: 0 < d by rewrite gcdn_gt0 m_gt0.
@@ -773,9 +769,8 @@ Proof. by move=> m n p q; rewrite -!gcdnA (gcdnCA n). Qed.
 Lemma muln_gcdr : right_distributive muln gcdn.
 Proof.
 move=> p m n; case: (posnP p) => [-> //| p_gt0].
-elim: {m}m.+1 {-2}m n (ltnSn m) => // s IHs m n; rewrite ltnS => le_ms.
-rewrite gcdnE [rhs in _ = rhs]gcdnE muln_eq0 (gtn_eqF p_gt0) -muln_modr //=.
-by case: posnP => // m_gt0; apply: IHs; apply: leq_trans le_ms; apply: ltn_pmod.
+elim/ltn_ind: m n => m IHm n; rewrite gcdnE [RHS]gcdnE muln_eq0 (gtn_eqF p_gt0).
+by case: posnP => // m_gt0; rewrite -muln_modr //=; apply/IHm/ltn_pmod.
 Qed.
 
 Lemma muln_gcdl : left_distributive muln gcdn.
@@ -825,8 +820,9 @@ Proof. by move=> m n p; rewrite -!(mulnC p) muln_lcmr. Qed.
 
 Lemma lcmnA : associative lcmn.
 Proof.
-move=> m n p; rewrite {1 3}/lcmn mulnC !divn_mulAC ?dvdn_mull ?dvdn_gcdr //.
-rewrite -!divnMA ?dvdn_mulr ?dvdn_gcdl // mulnC mulnA !muln_gcdr.
+move=> m n p; rewrite [LHS]/lcmn [RHS]/lcmn mulnC.
+rewrite !divn_mulAC ?dvdn_mull ?dvdn_gcdr // -!divnMA ?dvdn_mulr ?dvdn_gcdl //.
+rewrite mulnC mulnA !muln_gcdr; congr (_ %/ _).
 by rewrite ![_ * lcmn _ _]mulnC !muln_lcm_gcd !muln_gcdl -!(mulnC m) gcdnA.
 Qed.
 
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 0da7a16..abdf23b 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -882,10 +882,11 @@ by rewrite ihss !size_cat size_merge size_cat -addnA addnCA -size_cat.
 Qed.
 
 Lemma sort_stable s :
-  sorted leT' s ->
+    sorted leT' s ->
   sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s).
 Proof.
-case: {-2}s (erefl s) => // x _ -> sorted_s; rewrite -(mkseq_nth x s) sort_map.
+move=> sorted_s; case Ds: s => // [x s1]; rewrite -{s1}Ds.
+rewrite -(mkseq_nth x s) sort_map.
 apply/(homo_sorted_in (f := nth x s)): (sort_iota_stable x s (size s)).
 move=> /= y z; rewrite !mem_sort !mem_iota !leq0n add0n /= => y_le_s z_le_s.
 case/andP => -> /= /implyP yz; apply/implyP => /yz {yz} y_le_z.
@@ -916,7 +917,7 @@ Qed.
 
 Lemma filter_sort p s : filter p (sort leT s) = sort leT (filter p s).
 Proof.
-case: {-2}s (erefl s) => // x _ ->.
+case Ds: s => // [x s1]; rewrite -{s1}Ds.
 rewrite -(mkseq_nth x s) !(filter_map, sort_map).
 congr map; apply/(@eq_sorted_irr _ (le_lex x s)) => //.
 - by move=> ?; rewrite /= ltnn implybF andbN.
@@ -935,7 +936,7 @@ Variables (leT_total : total leT) (leT_tr : transitive leT).
 Lemma mask_sort s m :
   {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)}.
 Proof.
-case: {-2}s (erefl s) => [|x _ ->]; first by case: m; exists [::].
+case Ds: {-}s => [|x s1]; [by rewrite Ds; case: m; exists [::] | clear s1 Ds].
 rewrite -(mkseq_nth x s) -map_mask !sort_map.
 exists [seq i \in mask m (iota 0 (size s)) |
             i <- sort (xrelpre (nth x s) leT) (iota 0 (size s))].
@@ -1059,8 +1060,8 @@ Qed.
 Lemma looping_uniq x n : uniq (traject f x n.+1) = ~~ looping x n.
 Proof.
 rewrite /looping; elim: n x => [|n IHn] x //.
-rewrite {-3}[n.+1]lock /= -lock {}IHn -iterSr -negb_or inE; congr (~~ _).
-apply: orb_id2r => /trajectP no_loop.
+rewrite [n.+1 in LHS]lock [iter]lock /= -!lock {}IHn -iterSr -negb_or inE.
+congr (~~ _); apply: orb_id2r => /trajectP no_loop.
 apply/idP/eqP => [/trajectP[m le_m_n def_x] | {1}<-]; last first.
   by rewrite iterSr -last_traject mem_last.
 have loop_m: looping x m.+1 by rewrite /looping iterSr -def_x mem_head.
@@ -1084,9 +1085,9 @@ Hypothesis Up : uniq p.
 Lemma prev_next : cancel (next p) (prev p).
 Proof.
 move=> x; rewrite prev_nth mem_next next_nth; case p_x: (x \in p) => //.
-case def_p: p Up p_x => // [y q]; rewrite -{-1}def_p => /= /andP[not_qy Uq] p_x.
-rewrite -{2}(nth_index y p_x); congr (nth y _ _); set i := index x p.
-have: i <= size q by rewrite -index_mem -/i def_p in p_x.
+case Dp: p Up p_x => // [y q]; rewrite [uniq _]/= -Dp => /andP[q'y Uq] p_x.
+rewrite -[RHS](nth_index y p_x); congr (nth y _ _); set i := index x p.
+have: i <= size q by rewrite -index_mem -/i Dp in p_x.
 case: ltngtP => // [lt_i_q|->] _; first by rewrite index_uniq.
 by apply/eqP; rewrite nth_default // eqn_leq index_size leqNgt index_mem.
 Qed.
@@ -1103,7 +1104,7 @@ Qed.
 
 Lemma cycle_next : fcycle (next p) p.
 Proof.
-case def_p: {-2}p Up => [|x q] Uq //.
+case def_p: p Up => [|x q] Uq //; rewrite -[in next _]def_p.
 apply/(pathP x)=> i; rewrite size_rcons => le_i_q.
 rewrite -cats1 -cat_cons nth_cat le_i_q /= next_nth {}def_p mem_nth //.
 rewrite index_uniq // nth_cat /= ltn_neqAle andbC -ltnS le_i_q.
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 1185e67..4e55abe 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -202,12 +202,12 @@ have{def_m bc def_bc ltc2 ltbc3}:
    let kb := (ifnz e k 1).*2 in
    [&& k > 0, p < m, lb_dvd p m, c < kb & lb_dvd p p || (e == 0)]
     /\ m + (b * kb + c).*2 = p ^ 2 + (a * p).*2.
-- rewrite -{-2}def_m; split=> //=; last first.
+- rewrite -def_m [in lb_dvd _ _]def_m; split=> //=; last first.
     by rewrite -def_bc addSn -doubleD 2!addSn -addnA subnKC // addnC.
   rewrite ltc2 /lb_dvd /index_iota /= dvdn2 -def_m.
   by rewrite [_.+2]lock /= odd_double.
-move: {2}a.+1 (ltnSn a) => n; clearbody k e.
-elim: n => // n IHn in a k p m b c e *; rewrite ltnS => le_a_n [].
+have [n] := ubnP a.
+elim: n => // n IHn in a (k) p m b c (e) * => /ltnSE-le_a_n [].
 set kb := _.*2; set d := _ + c => /and5P[lt0k ltpm leppm ltc pr_p def_m].
 have def_k1: k.-1.+1 = k := ltn_predK lt0k.
 have def_kb1: kb.-1.+1 = kb by rewrite /kb -def_k1; case e.
@@ -618,17 +618,17 @@ Lemma lognE p m :
   logn p m = if [&& prime p, 0 < m & p %| m] then (logn p (m %/ p)).+1 else 0.
 Proof.
 rewrite /logn /dvdn; case p_pr: (prime p) => //.
-rewrite /divn modn_def; case def_m: {2 3}m => [|m'] //=.
+case def_m: m => // [m']; rewrite !andTb [LHS]/= -def_m /divn modn_def.
 case: edivnP def_m => [[|q] [|r] -> _] // def_m; congr _.+1; rewrite [_.1]/=.
 have{m def_m}: q < m'.
   by rewrite -ltnS -def_m addn0 mulnC -{1}[q.+1]mul1n ltn_pmul2r // prime_gt1.
-elim: {m' q}_.+1 {-2}m' q.+1 (ltnSn m') (ltn0Sn q) => // s IHs.
-case=> [[]|r] //= m; rewrite ltnS => lt_rs m_gt0 le_mr.
-rewrite -{3}[m]prednK //=; case: edivnP => [[|q] [|_] def_q _] //.
-have{def_q} lt_qm': q < m.-1.
-  by rewrite -[q.+1]muln1 -ltnS prednK // def_q addn0 ltn_pmul2l // prime_gt1.
-have{le_mr} le_m'r: m.-1 <= r by rewrite -ltnS prednK.
-by rewrite (IHs r) ?(IHs m.-1) // ?(leq_trans lt_qm', leq_trans _ lt_rs).
+elim/ltn_ind: m' {q}q.+1 (ltn0Sn q) => -[_ []|r IHr m] //= m_gt0 le_mr.
+rewrite -[m in logn_rec _ _ m]prednK //=.
+case: edivnP => [[|q] [|_] def_q _] //; rewrite addn0 in def_q.
+have{def_q} lt_qm1: q < m.-1.
+  by rewrite -[q.+1]muln1 -ltnS prednK // def_q ltn_pmul2l // prime_gt1.
+have{le_mr} le_m1r: m.-1 <= r by rewrite -ltnS prednK.
+by rewrite (IHr r) ?(IHr m.-1) // (leq_trans lt_qm1).
 Qed.
 
 Lemma logn_gt0 p n : (0 < logn p n) = (p \in primes n).
@@ -803,9 +803,10 @@ Lemma trunc_log_bounds p n :
   1 < p -> 0 < n -> let k := trunc_log p n in p ^ k <= n < p ^ k.+1.
 Proof.
 rewrite {+}/trunc_log => p_gt1; have p_gt0 := ltnW p_gt1.
-elim: n {-2 5}n (leqnn n) => [|m IHm] [|n] //=; rewrite ltnS => le_n_m _.
+set loop := (loop in loop n n); set m := n; rewrite [in n in loop m n]/m.
+have: m <= n by []; elim: n m => [|n IHn] [|m] //= /ltnSE-le_m_n _.
 have [le_p_n | // ] := leqP p _; rewrite 2!expnSr -leq_divRL -?ltn_divLR //.
-by apply: IHm; rewrite ?divn_gt0 // -ltnS (leq_trans (ltn_Pdiv _ _)).
+by apply: IHn; rewrite ?divn_gt0 // -ltnS (leq_trans (ltn_Pdiv _ _)).
 Qed.
 
 Lemma trunc_log_ltn p n : 1 < p -> n < p ^ (trunc_log p n).+1.
@@ -1368,7 +1369,7 @@ Qed.
 
 Lemma totient_count_coprime n : totient n = \sum_(0 <= d < n) coprime n d.
 Proof.
-elim: {n}_.+1 {-2}n (ltnSn n) => // m IHm n; rewrite ltnS => le_n_m.
+elim/ltn_ind: n => // n IHn.
 case: (leqP n 1) => [|lt1n]; first by rewrite unlock; case: (n) => [|[]].
 pose p := pdiv n; have p_pr: prime p by apply: pdiv_prime.
 have p1 := prime_gt1 p_pr; have p0 := ltnW p1.
@@ -1378,11 +1379,10 @@ have [n0 np0 np'0]: [/\ n > 0, np > 0 & np' > 0] by rewrite ltnW ?part_gt0.
 have def_n: n = np * np' by rewrite partnC.
 have lnp0: 0 < logn p n by rewrite lognE p_pr n0 pdiv_dvd.
 pose in_mod k (k0 : k > 0) d := Ordinal (ltn_pmod d k0).
-rewrite {1}def_n totient_coprime // {IHm}(IHm np') ?big_mkord; last first.
-  apply: leq_trans le_n_m; rewrite def_n ltn_Pmull //.
-  by rewrite /np p_part -(expn0 p) ltn_exp2l.
+rewrite {1}def_n totient_coprime // {IHn}(IHn np') ?big_mkord; last first.
+  by rewrite def_n ltn_Pmull // /np p_part -(expn0 p) ltn_exp2l.
 have ->: totient np = #|[pred d : 'I_np | coprime np d]|.
-  rewrite {1}[np]p_part totient_pfactor //=; set q := p ^ _.
+  rewrite [np in LHS]p_part totient_pfactor //=; set q := p ^ _.
   apply: (@addnI (1 * q)); rewrite -mulnDl [1 + _]prednK // mul1n.
   have def_np: np = p * q by rewrite -expnS prednK // -p_part.
   pose mulp := [fun d : 'I_q => in_mod _ np0 (p * d)].
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 74b3f15..5566a44 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1453,7 +1453,7 @@ Definition perm_eq s1 s2 :=
 Lemma permP s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2).
 Proof.
 apply: (iffP allP) => /= [eq_cnt1 a | eq_cnt x _]; last exact/eqP.
-elim: {a}_.+1 {-2}a (ltnSn (count a (s1 ++ s2))) => // n IHn a le_an.
+have [n le_an] := ubnP (count a (s1 ++ s2)); elim: n => // n IHn in a le_an *. 
 have [/eqP|] := posnP (count a (s1 ++ s2)).
   by rewrite count_cat addn_eq0; do 2!case: eqP => // ->.
 rewrite -has_count => /hasP[x s12x a_x]; pose a' := predD1 a x.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index d47a3ba..9f826aa 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -400,6 +400,51 @@ Proof. by move=> lt_mn /ltnW; apply: leq_trans. Qed.
 Lemma leq_total m n : (m <= n) || (m >= n).
 Proof. by rewrite -implyNb -ltnNge; apply/implyP; apply: ltnW. Qed.
 
+(* Helper lemmas to support generalized induction over a nat measure.         *)
+(* The idiom for a proof by induction over a measure Mxy : nat involving      *)
+(* variables x, y, ... (e.g., size x + size y) is                             *)
+(*   have [m leMn] := ubnP Mxy; elim: n => // n IHn in x y ... leMn ... *.    *)
+(* after which the current goal (possibly modified by generalizations in the  *)
+(* in ... part) can be proven with the extra context assumptions              *)
+(*  n : nat                                                                   *)
+(*  IHn : forall x y ..., Mxy < n -> ... -> the_initial_goal                  *)
+(*  leMn : Mxy < n.+1                                                         *)
+(* This is preferable to the legacy idiom relying on numerical occurrence     *)
+(* selection, which is fragile if there can be multiple occurrences of x, y,  *)
+(* ... in the measure expression Mxy (e.g., in #|y| with x : finType and      *)
+(* y : {set x}).                                                              *)
+(*  The leMn statement is convertible to Mxy <= n; if it is necessary to      *)
+(* have _exactly_ leMn : Mxy <= n, the ltnSE helper lemma may be used as      *)
+(* follows                                                                    *)
+(*   have [m] := ubnP Mxy; elim: n => // n IHn in x y ... * => /ltnSE-leMn.   *)
+(*  We also provide alternative helper lemmas for proofs where the upper      *)
+(* bound appears in the goal, and we assume nonstrict (in)equality.           *)
+(* In either case the proof will have to dispatch an Mxy = 0 case.            *)
+(*  have [m defM] := ubnPleq Mxy; elim: n => [|n IHn] in x y ... defM ... *.  *)
+(* yields two subgoals, in which Mxy has been replaced by 0 and n.+1,         *)
+(* with the extra assumption defM : Mxy <= 0 / Mxy <= n.+1, respectively.     *)
+(* The second goal also has the inductive assumption                          *)
+(*   IHn : forall x y ..., Mxy <= n -> ... -> the_initial_goal[n / Mxy].      *)
+(* Using ubnPgeq or ubnPeq instead of ubnPleq yields assumptions with         *)
+(* Mxy >= 0/n.+1 or Mxy == 0/n.+1 instead of Mxy <= 0/n.+1, respectively.     *)
+(* These introduce a different kind of induction; for example ubnPgeq M lets  *)
+(* us remember that n < M throughout the induction.                           *)
+(*   Finally, the ltn_ind lemma provides a generalized induction view for a   *)
+(* property of a single integer (i.e., the case Mxy := x).                    *)
+Lemma ubnP m : {n | m < n}.             Proof. by exists m.+1. Qed.
+Lemma ltnSE m n : m < n.+1 -> m <= n.   Proof. by []. Qed.
+Variant ubn_leq_spec m : nat -> Type := UbnLeq n of m <= n : ubn_leq_spec m n.
+Variant ubn_geq_spec m : nat -> Type := UbnGeq n of m >= n : ubn_geq_spec m n.
+Variant ubn_eq_spec m : nat -> Type := UbnEq n of m == n : ubn_eq_spec m n.
+Lemma ubnPleq m : ubn_leq_spec m m.    Proof. by []. Qed.
+Lemma ubnPgeq m : ubn_geq_spec m m.    Proof. by []. Qed.
+Lemma ubnPeq m : ubn_eq_spec m m.      Proof. by []. Qed.
+Lemma ltn_ind P : (forall n, (forall m, m < n -> P m) -> P n) -> forall n, P n.
+Proof.
+move=> accP M; have [n leMn] := ubnP M; elim: n => // n IHn in M leMn *.
+by apply/accP=> p /leq_trans/(_ leMn)/IHn.
+Qed.
+
 (* Link to the legacy comparison predicates. *)
 
 Lemma leP m n : reflect (m <= n)%coq_nat (m <= n).
@@ -412,15 +457,14 @@ Arguments leP {m n}.
 
 Lemma le_irrelevance m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m <= n)%coq_nat.
 Proof.
-elim: {n}n.+1 {-1}n (erefl n.+1) => // n IHn _ [<-] in le_mn1 le_mn2 *.
-pose def_n2 := erefl n; transitivity (eq_ind _ _ le_mn2 _ def_n2) => //.
-move def_n1: {1 4 5 7}n le_mn1 le_mn2 def_n2 => n1 le_mn1.
-case: n1 / le_mn1 def_n1 => [|n1 le_mn1] def_n1 [|n2 le_mn2] def_n2.
-- by rewrite [def_n2]eq_axiomK.
-- by move/leP: (le_mn2); rewrite -{1}def_n2 ltnn.
-- by move/leP: (le_mn1); rewrite {1}def_n2 ltnn.
-case: def_n2 (def_n2) => ->{n2} def_n2 in le_mn2 *.
-by rewrite [def_n2]eq_axiomK /=; congr le_S; apply: IHn.
+elim/ltn_ind: n => n IHn in le_mn1 le_mn2 *; set n1 := n in le_mn1 *.
+pose def_n : n = n1 := erefl n; transitivity (eq_ind _ _ le_mn2 _ def_n) => //.
+case: n1 / le_mn1 le_mn2 => [|n1 le_mn1] {n}[|n le_mn2] in (def_n) IHn *.
+- by rewrite [def_n]eq_axiomK.
+- by case/leP/idPn: (le_mn2); rewrite -def_n ltnn.
+- by case/leP/idPn: (le_mn1); rewrite def_n ltnn.
+case: def_n (def_n) => <-{n1} def_n in le_mn1 *.
+by rewrite [def_n]eq_axiomK /=; congr le_S; apply: IHn.
 Qed.
 
 Lemma ltP m n : reflect (m < n)%coq_nat (m < n).
@@ -1681,7 +1725,7 @@ Definition bin_of_nat n0 := if n0 is n.+1 then Npos (pos_of_nat n n) else 0%num.
 Lemma bin_of_natK : cancel bin_of_nat nat_of_bin.
 Proof.
 have sub2nn n : n.*2 - n = n by rewrite -addnn addKn.
-case=> //= n; rewrite -{3}[n]sub2nn.
+case=> //= n; rewrite -[n in RHS]sub2nn.
 by elim: n {2 4}n => // m IHm [|[|n]] //=; rewrite IHm // natTrecE sub2nn.
 Qed.