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.

7 files changed, 72 insertions, 81 deletions

diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 122457d..7663e63 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -909,7 +909,7 @@ wlog Dj: j M nzMij / j = 0; last rewrite {j}Dj in nzMij.
      by rewrite xcolE unitmx_mul uR unitmx_perm.
   by rewrite xcolE !mulmxA -dM xcolE -mulmxA -perm_mxM tperm2 perm_mx1 mulmx1.
 move Da: (M i 0) nzMij => a nz_a.
-elim: {a}_.+1 {-2}a (ltnSn `|a|) => // A IHa a leA in m n M i Da nz_a le_mn *.
+have [A leA] := ubnP `|a|; elim: A => // A IHa in a leA m n M i Da nz_a le_mn *.
 wlog [j a'Mij]: m n M i Da le_mn / {j | ~~ (a %| M i j)%Z}; last first.
   have nz_j: j != 0 by apply: contraNneq a'Mij => ->; rewrite Da.
   case: n => [[[]//]|n] in j le_mn nz_j M a'Mij Da *.
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index a39aba1..38beffc 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -877,9 +877,9 @@ Lemma mxrank_leqif_sup m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
 Proof.
 move=> sAB; split; first by rewrite mxrankS.
 apply/idP/idP=> [| sBA]; last by rewrite eqn_leq !mxrankS.
-case/submxP: sAB => D ->; rewrite -{-2}(mulmx_base B) mulmxA.
+case/submxP: sAB => D ->; set r := \rank B; rewrite -(mulmx_base B) mulmxA.
 rewrite mxrankMfree // => /row_fullP[E kE].
-by rewrite -{1}[row_base B]mul1mx -kE -(mulmxA E) (mulmxA _ E) submxMl.
+by rewrite -[rB in _ *m rB]mul1mx -kE -(mulmxA E) (mulmxA _ E) submxMl.
 Qed.
 
 Lemma mxrank_leqif_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
@@ -1100,7 +1100,7 @@ Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) :
 Proof.
 apply: (iffP idP) => [| [u_ ->]]; last first.
   by apply: summx_sub_sums => i _; apply: submxMl.
-elim: {P}_.+1 {-2}P A (ltnSn #|P|) => // b IHb P A.
+have [b] := ubnP #|P|; elim: b => // b IHb in P A *.
 case: (pickP P) => [i Pi | P0 _]; last first.
   rewrite big_pred0 //; move/submx0null->.
   by exists (fun _ => 0); rewrite big_pred0.
@@ -1579,7 +1579,9 @@ Qed.
 
 Lemma proj_mx_proj n (U V : 'M_n) :
   let P := proj_mx U V in (U :&: V = 0)%MS -> P *m P = P.
-Proof. by move=> P dxUV; rewrite -{-2}[P]mul1mx proj_mx_id ?proj_mx_sub. Qed.
+Proof.
+by move=> P dxUV; rewrite -[P in P *m _]mul1mx proj_mx_id ?proj_mx_sub ?mul1mx.
+Qed.
 
 (* Completing a partially injective matrix to get a unit matrix. *)
 
@@ -1845,7 +1847,8 @@ rewrite /TIsum; apply: (iffP eqnP) => /= [dxS i Pi | dxS].
   set Si' := (\sum_(j | _) unwrap (S_ j))%MS.
   have: mxdirect (unwrap (S_ i) + Si') by apply/eqnP; rewrite /= -!(bigD1 i).
   by rewrite mxdirect_addsE => /and3P[-> _ /eqP].
-elim: _.+1 {-2 4}P (subxx P) (ltnSn #|P|) => // m IHm Q; move/subsetP=> sQP.
+set Q := P; have [m] := ubnP #|Q|; have: Q \subset P by [].
+elim: m Q => // m IHm Q /subsetP-sQP.
 case: (pickP Q) => [i Qi | Q0]; last by rewrite !big_pred0 ?mxrank0.
 rewrite (cardD1x Qi) !((bigD1 i) Q) //=.
 move/IHm=> <- {IHm}/=; last by apply/subsetP=> j /andP[/sQP].
@@ -1946,7 +1949,7 @@ Proof. by apply: (iffP (rowV0Pn _)) => [] [v]; move/eigenspaceP; exists v. Qed.
 Lemma mxdirect_sum_eigenspace (P : pred I) a_ :
   {in P &, injective a_} -> mxdirect (\sum_(i | P i) eigenspace (a_ i)).
 Proof.
-elim: {P}_.+1 {-2}P (ltnSn #|P|) => // m IHm P lePm inj_a.
+have [m] := ubnP #|P|; elim: m P => // m IHm P lePm inj_a.
 apply/mxdirect_sumsP=> i Pi; apply/eqP/rowV0P => v.
 rewrite sub_capmx => /andP[/eigenspaceP def_vg].
 set Vi' := (\sum_(i | _) _)%MS => Vi'v.
@@ -2109,9 +2112,9 @@ Proof.
 case: n => // n' _; set n := n'.+1; set p := #|F|.
 rewrite big_nat_rev big_add1 -triangular_sum expn_sum -big_split /=.
 pose fr m := [pred A : 'M[F]_(m, n) | \rank A == m].
-set m := {-7}n; transitivity #|fr m|.
+set m := n; rewrite [in m.+1]/m; transitivity #|fr m|.
   by rewrite cardsT /= card_sub; apply: eq_card => A; rewrite -row_free_unit.
-elim: m (leqnn m : m <= n) => [_|m IHm]; last move/ltnW=> le_mn.
+have: m <= n by []; elim: m => [_ | m IHm /ltnW-le_mn].
   rewrite (@eq_card1 _ (0 : 'M_(0, n))) ?big_geq //= => A.
   by rewrite flatmx0 !inE !eqxx.
 rewrite big_nat_recr // -{}IHm //= !subSS mulnBr muln1 -expnD subnKC //.
@@ -2453,7 +2456,7 @@ Definition cent_mx_fun (B : 'M[F]_n) := R *m lin_mx (mulmxr B \- mulmx B).
 Lemma cent_mx_fun_is_linear : linear cent_mx_fun.
 Proof.
 move=> a A B; apply/row_matrixP=> i; rewrite linearP row_mul mul_rV_lin.
-rewrite /= {-3}[row]lock row_mul mul_rV_lin -lock row_mul mul_rV_lin.
+rewrite /= [row i _ as v in a *: v]row_mul mul_rV_lin row_mul mul_rV_lin.
 by rewrite -linearP -(linearP [linear of mulmx _ \- mulmxr _]).
 Qed.
 Canonical cent_mx_fun_additive := Additive cent_mx_fun_is_linear.
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index b95933e..861a7df 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -179,13 +179,13 @@ have{Ss u} ->: Ss = Ss_ dS.
       by rewrite ltn_subRL (leq_trans _ k_ge_dS) // addnC ltn_add2l.
   by rewrite insubdK //; case: (split i) => {i}i;
      rewrite !mxE coefMXn; case: leqP.
-elim: {-2}dS (leqnn dS) (dS_gt0) => // dj IHj dj_lt_dS _.
-pose j1 := Ordinal dj_lt_dS; pose rj0T (A : 'M[{poly R}]_dS) := row j0 A^T.
+case: (ubnPgeq dS) (dS_gt0); elim=> // dj IHj ltjS _; pose j1 := Ordinal ltjS.
+pose rj0T (A : 'M[{poly R}]_dS) := row j0 A^T.
 have: rj0T (Ss_ dj.+1) = 'X^dj *: rj0T (S_ j1) + 1 *: rj0T (Ss_ dj).
   apply/rowP=> i; apply/polyP=> k; rewrite scale1r !(Sylvester_mxE, mxE) eqxx.
   rewrite coefD coefXnM coefC !coef_poly ltnS subn_eq0 ltn_neqAle andbC.
   case: (leqP k dj) => [k_le_dj | k_gt_dj] /=; last by rewrite addr0.
-  rewrite Sylvester_mxE insubdK; last exact: leq_ltn_trans (dj_lt_dS).
+  rewrite Sylvester_mxE insubdK; last exact: leq_ltn_trans (ltjS).
   by case: eqP => [-> | _]; rewrite (addr0, add0r).
 rewrite -det_tr => /determinant_multilinear->;
   try by apply/matrixP=> i j; rewrite !mxE eq_sym (negPf (neq_lift _ _)).
@@ -858,8 +858,8 @@ have{mon_p pw0 intRp intRq}: genI S.
   split; set S1 := _ ++ _; first exists p.
     split=> // i; rewrite -[p]coefK coef_poly; case: ifP => // lt_i_p.
     by apply: genS; rewrite mem_cat orbC mem_nth.
-  have: all (mem S1) S1 by apply/allP.
-  elim: {-1}S1 => //= y S2 IH /andP[S1y S12]; split; last exact: IH.
+  set S2 := S1; have: all (mem S1) S2 by apply/allP.
+  elim: S2 => //= y S2 IH /andP[S1y S12]; split; last exact: IH.
   have{q S S1 IH S1y S12 intRp intRq} [q mon_q qx0]: integralOver RtoK y.
     by move: S1y; rewrite mem_cat => /orP[]; [apply: intRq | apply: intRp].
   exists (map_poly RtoK q); split=> // [|i]; first exact: monic_map.
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index eb96da2..2bb3614 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -1172,14 +1172,14 @@ Qed.
 Lemma multiplicity_XsubC p a :
   {m | exists2 q, (p != 0) ==> ~~ root q a & p = q * ('X - a%:P) ^+ m}.
 Proof.
-elim: {p}(size p) {-2}p (eqxx (size p)) => [|n IHn] p.
-  by rewrite size_poly_eq0 => ->; exists 0%N, p; rewrite ?mulr1.
-have [/sig_eqW[{p}p ->] sz_p | nz_pa] := altP (factor_theorem p a); last first.
-  by exists 0%N, p; rewrite ?mulr1 ?nz_pa ?implybT.
-have nz_p: p != 0 by apply: contraTneq sz_p => ->; rewrite mul0r size_poly0.
-rewrite size_Mmonic ?monicXsubC // size_XsubC addn2 eqSS in sz_p.
-have [m /sig2_eqW[q nz_qa Dp]] := IHn p sz_p; rewrite nz_p /= in nz_qa.
-by exists m.+1, q; rewrite ?nz_qa ?implybT // exprSr mulrA -Dp.
+have [n le_p_n] := ubnP (size p); elim: n => // n IHn in p le_p_n *.
+have [-> | nz_p /=] := eqVneq p 0; first by exists 0%N, 0; rewrite ?mul0r.
+have [/sig_eqW[p1 Dp] | nz_pa] := altP (factor_theorem p a); last first.
+  by exists 0%N, p; rewrite ?mulr1.
+have nz_p1: p1 != 0 by apply: contraNneq nz_p => p1_0; rewrite Dp p1_0 mul0r.
+have /IHn[m /sig2_eqW[q nz_qa Dp1]]: size p1 < n.
+  by rewrite Dp size_Mmonic ?monicXsubC // size_XsubC addn2 in le_p_n. 
+by exists m.+1, q; [rewrite nz_p1 in nz_qa | rewrite exprSr mulrA -Dp1].
 Qed.
 
 (* Roots of unity. *)
@@ -2691,17 +2691,15 @@ Proof.
 pose polyT (p : seq F) := (foldr (fun c f => f * 'X_0 + c%:T) (0%R)%:T p)%T.
 have eval_polyT (q : {poly F}) x : GRing.eval [:: x] (polyT q) = q.[x].
   by rewrite /horner; elim: (val q) => //= ? ? ->.
-elim: size {-2}p (leqnn (size p)) => {p} [p|n IHn p].
-  by move=> /size_poly_leq0P->; exists [::], 0; rewrite mul0r eqxx.
+have [n] := ubnP (size p); elim: n => // n IHn in p *.
 have /decPcases /= := @satP F [::] ('exists 'X_0, polyT p == 0%T).
 case: ifP => [_ /sig_eqW[x]|_ noroot]; last first.
   exists [::], p; rewrite big_nil mulr1; split => // p_neq0 x.
   by apply/negP=> /rootP rpx; apply noroot; exists x; rewrite eval_polyT.
-rewrite eval_polyT => /rootP /factor_theorem /sig_eqW [q ->].
-have [->|q_neq0] := eqVneq q 0; first by exists [::], 0; rewrite !mul0r eqxx.
-rewrite size_mul ?polyXsubC_eq0 // ?size_XsubC addn2 /= ltnS => sq_le_n.
-have [] // := IHn q => s [r [-> nr]]; exists (s ++ [::x]), r.
-by rewrite big_cat /= big_seq1 mulrA.
+rewrite eval_polyT => /rootP/factor_theorem/sig_eqW[p1 ->].
+have [->|nz_p1] := eqVneq p1 0; first by exists [::], 0; rewrite !mul0r eqxx.
+rewrite size_Mmonic ?monicXsubC // size_XsubC addn2 => /IHn[s [q [-> irr_q]]].
+by exists (rcons s x), q; rewrite -cats1 big_cat big_seq1 mulrA.
 Qed.
 
 End DecField.
@@ -2717,7 +2715,7 @@ Lemma closed_rootP p : reflect (exists x, root p x) (size p != 1%N).
 Proof.
 have [-> | nz_p] := eqVneq p 0.
   by rewrite size_poly0; left; exists 0; rewrite root0.
-rewrite neq_ltn {1}polySpred //=.
+rewrite neq_ltn [in _ < 1]polySpred //=.
 apply: (iffP idP) => [p_gt1 | [a]]; last exact: root_size_gt1.
 pose n := (size p).-1; have n_gt0: n > 0 by rewrite -ltnS -polySpred.
 have [a Dan] := closedF (fun i => - p`_i / lead_coef p) n_gt0.
diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v
index e91b8be..9bc8fd5 100644
--- a/mathcomp/algebra/polyXY.v
+++ b/mathcomp/algebra/polyXY.v
@@ -374,7 +374,7 @@ move=> nz_px [q nz_q qx0].
 have [/size1_polyC Dp | p_gt1] := leqP (size p) 1.
   by rewrite {}/pEx Dp map_polyC hornerC map_poly_eq0 in nz_px *; exists p`_0.
 have nz_p: p != 0 by rewrite -size_poly_gt0 ltnW.
-elim: {q}_.+1 {-2}q (ltnSn (size q)) => // m IHm q le_qm in nz_q qx0 *.
+have [m le_qm] := ubnP (size q); elim: m => // m IHm in q le_qm nz_q qx0 *.
 have nz_q1: q^:P != 0 by rewrite map_poly_eq0.
 have sz_q1: size q^:P = size q by rewrite size_map_polyC.
 have q1_gt1: size q^:P > 1.
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index aa076a2..6b5d003 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -1728,18 +1728,16 @@ Proof. by move=> p; rewrite gcdpE ltnn modpp gcd0p. Qed.
 
 Lemma dvdp_gcdlr p q : (gcdp p q %| p) && (gcdp p q %| q).
 Proof.
-elim: {p q}minn {-2}p {-2}q (leqnn (minn (size q) (size p))) => [|r Hrec] p q.
-  rewrite geq_min !leqn0 !size_poly_eq0.
-  by case/pred2P=> ->; rewrite (gcdp0, gcd0p) dvdpp ?andbT /=.
-case: (eqVneq p 0) => [-> _|nz_p]; first by rewrite gcd0p dvdpp andbT.
-case: (eqVneq q 0) => [->|nz_q]; first by rewrite gcdp0 dvdpp /=.
-rewrite gcdpE minnC /minn; case: ltnP => [lt_pq | le_pq] le_qr.
-  suffices: minn (size p) (size (q %% p)) <= r.
-    by move/Hrec; case/andP => E1 E2; rewrite E2 (dvdp_mod _ E2).
-  by rewrite geq_min orbC -ltnS (leq_trans _ le_qr) ?ltn_modp.
-suffices: minn (size q) (size (p %% q)) <= r.
-  by move/Hrec; case/andP => E1 E2; rewrite E2 andbT (dvdp_mod _ E2).
-by rewrite geq_min orbC -ltnS (leq_trans _ le_qr) ?ltn_modp.
+have [r] := ubnP (minn (size q) (size p)); elim: r => // r IHr in p q *.
+have [-> | nz_p] := eqVneq p 0; first by rewrite gcd0p dvdpp andbT.
+have [-> | nz_q] := eqVneq q 0; first by rewrite gcdp0 dvdpp /=.
+rewrite ltnS gcdpE minnC /minn; case: ltnP => [lt_pq | le_pq] le_qr.
+  suffices /IHr/andP[E1 E2]: minn (size p) (size (q %% p)) < r.
+    by rewrite E2 (dvdp_mod _ E2).
+  by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp.
+suffices /IHr/andP[E1 E2]: minn (size q) (size (p %% q)) < r.
+  by rewrite E2 andbT (dvdp_mod _ E2).
+by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp.
 Qed.
 
 Lemma dvdp_gcdl p q : gcdp p q %| p.
@@ -1756,22 +1754,18 @@ Proof. by move=> qn0; move: (dvdp_gcdr p q); apply: dvdp_leq. Qed.
 
 Lemma dvdp_gcd p m n : p %| gcdp m n = (p %| m) && (p %| n).
 Proof.
-apply/idP/andP=> [dv_pmn | [dv_pm dv_pn]].
+apply/idP/andP=> [dv_pmn | []].
   by rewrite ?(dvdp_trans dv_pmn) ?dvdp_gcdl ?dvdp_gcdr.
-move: (leqnn (minn (size n) (size m))) dv_pm dv_pn.
-elim: {m n}minn {-2}m {-2}n => [|r Hrec] m n.
-  rewrite geq_min !leqn0 !size_poly_eq0.
-  by case/pred2P=> ->; rewrite (gcdp0, gcd0p).
-case: (eqVneq m 0) => [-> _|nz_m]; first by rewrite gcd0p /=.
-case: (eqVneq n 0) => [->|nz_n]; first by rewrite gcdp0 /=.
-rewrite gcdpE minnC /minn; case: ltnP => Cnm le_r dv_m dv_n.
-  apply: Hrec => //; last by rewrite -(dvdp_mod _ dv_m).
-  by rewrite geq_min orbC -ltnS (leq_trans _ le_r) ?ltn_modp.
-apply: Hrec => //; last by rewrite -(dvdp_mod _ dv_n).
-by rewrite geq_min orbC -ltnS (leq_trans _ le_r) ?ltn_modp.
+have [r] := ubnP (minn (size n) (size m)); elim: r => // r IHr in m n *.
+have [-> | nz_m] := eqVneq m 0; first by rewrite gcd0p.
+have [-> | nz_n] := eqVneq n 0; first by rewrite gcdp0.
+rewrite gcdpE minnC ltnS /minn; case: ltnP => [lt_mn | le_nm] le_r dv_m dv_n.
+  apply: IHr => //; last by rewrite -(dvdp_mod _ dv_m).
+  by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp.
+apply: IHr => //; last by rewrite -(dvdp_mod _ dv_n).
+by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp.
 Qed.
 
-
 Lemma gcdpC : forall p q, gcdp p q %= gcdp q p.
 Proof. by move=> p q; rewrite /eqp !dvdp_gcd !dvdp_gcdl !dvdp_gcdr. Qed.
 
@@ -3233,24 +3227,19 @@ Qed.
 
 Lemma dvdp_gdcor p q : q != 0 -> p %| (gdcop q p) * (q ^+ size p).
 Proof.
-move=> q_neq0; rewrite /gdcop.
-elim: (size p) {-2 5}p (leqnn (size p))=> {p} [|n ihn] p.
-  rewrite size_poly_leq0; move/eqP->.
-  by rewrite size_poly0 /= dvd0p expr0 mulr1 (negPf q_neq0).
-move=> hsp /=; have [->|p_neq0] := altP (p =P 0).
-  rewrite size_poly0 /= dvd0p expr0 mulr1 div0p /=.
-  case: ifP=> // _; have := (ihn 0).
-  by rewrite size_poly0 expr0 mulr1 dvd0p=> /(_ isT).
-have [|ncop_pq] := boolP (coprimep _ _); first by rewrite dvdp_mulr ?dvdpp.
-have g_gt1: (1 < size (gcdp p q))%N.
-  have [//||/esym/eqP] := ltngtP; last by rewrite -coprimep_def (negPf ncop_pq).
-  by rewrite ltnS leqn0 size_poly_eq0 gcdp_eq0 (negPf p_neq0).
-have sd : (size (p %/ gcdp p q) < size p)%N.
+rewrite /gdcop => nz_q; have [n hsp] := ubnPleq (size p).
+elim: n => [|n IHn] /= in p hsp *; first by rewrite (negPf nz_q) mul0r dvdp0.
+have [_ | ncop_pq] := ifPn; first by rewrite dvdp_mulr.
+have g_gt1: 1 < size (gcdp p q).
+  rewrite ltn_neqAle eq_sym ncop_pq lt0n size_poly_eq0 gcdp_eq0.
+  by rewrite negb_and nz_q orbT.
+have [-> | nz_p] := eqVneq p 0.
+  by rewrite div0p exprSr mulrA dvdp_mulr // IHn // size_poly0.
+have le_d_p: size (p %/ gcdp p q) < size p.
   rewrite size_divp -?size_poly_eq0 -(subnKC g_gt1) // add2n /=.
-  by rewrite -[size _]prednK ?size_poly_gt0 // ltnS subSS leq_subr.
-rewrite -{1}[p](divpK (dvdp_gcdl _ q)) -(subnKC sd) addSnnS exprD mulrA.
-rewrite dvdp_mul ?ihn //; first by rewrite -ltnS (leq_trans sd).
-by rewrite exprS dvdp_mulr // dvdp_gcdr.
+  by rewrite polySpred // ltnS subSS leq_subr.
+rewrite -[p in p %| _](divpK (dvdp_gcdl p q)) exprSr mulrA.
+by rewrite dvdp_mul ?IHn ?dvdp_gcdr // -ltnS (leq_trans le_d_p).
 Qed.
 
 Lemma reducible_cubic_root p q :
@@ -3291,8 +3280,8 @@ Lemma redivp_map a b :
   redivp a^f b^f = (rscalp a b, (rdivp a b)^f, (rmodp a b)^f).
 Proof.
 rewrite /rdivp /rscalp /rmodp !unlock map_poly_eq0 size_map_poly.
-case: eqP; rewrite /= -(rmorph0 (map_poly_rmorphism f)) //; move/eqP=> q_nz.
-move: (size a) => m; elim: m 0%N 0 a => [|m IHm] qq r a /=.
+have [// | q_nz] := ifPn; rewrite -(rmorph0 (map_poly_rmorphism f)) //.
+have [m _] := ubnPeq (size a); elim: m 0%N 0 a => [|m IHm] qq r a /=.
   rewrite -!mul_polyC  !size_map_poly !lead_coef_map // -(map_polyXn f).
   by rewrite -!(map_polyC f) -!rmorphM -rmorphB -rmorphD; case: (_ < _).
 rewrite -!mul_polyC !size_map_poly !lead_coef_map // -(map_polyXn f).
@@ -3359,9 +3348,9 @@ wlog lt_p_q: p q / size p < size q.
   rewrite gcdpE (gcdpE p^f) !size_map_poly ltnNge le_q_p /= -map_modp.
   case: (eqVneq q 0) => [-> | q_nz]; first by rewrite rmorph0 !gcdp0.
   by rewrite IHpq ?ltn_modp.
-elim: {q}_.+1 p {-2}q (ltnSn (size q)) lt_p_q => // m IHm p q le_q_m lt_p_q.
+have [m le_q_m] := ubnP (size q); elim: m => // m IHm in p q lt_p_q le_q_m *.
 rewrite gcdpE (gcdpE p^f) !size_map_poly lt_p_q -map_modp.
-case: (eqVneq p 0) => [-> | q_nz]; first by rewrite rmorph0 !gcdp0.
+have [-> | q_nz] := eqVneq p 0; first by rewrite rmorph0 !gcdp0.
 by rewrite IHm ?(leq_trans lt_p_q) ?ltn_modp.
 Qed.
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index f8c5675..495ce18 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -3185,7 +3185,7 @@ Lemma lerif_AGM_scaled (I : finType) (A : {pred I}) (E : I -> R) (n := #|A|) :
   \prod_(i in A) (E i *+ n) <= (\sum_(i in A) E i) ^+ n
                             ?= iff [forall i in A, forall j in A, E i == E j].
 Proof.
-elim: {A}_.+1 {-2}A (ltnSn #|A|) => // m IHm A leAm in E n * => Ege0.
+have [m leAm] := ubnP #|A|; elim: m => // m IHm in A leAm E n * => Ege0.
 apply/lerifP; case: ifPn => [/forall_inP-Econstant | Enonconstant].
   have [i /= Ai | A0] := pickP (mem A); last by rewrite [n]eq_card0 ?big_pred0.
   have /eqfun_inP-E_i := Econstant i Ai; rewrite -(eq_bigr _ E_i) sumr_const.
@@ -4990,8 +4990,9 @@ Qed.
 Lemma normC_sub_eq x y :
   `|x - y| = `|x| - `|y| -> {t | `|t| == 1 & (x, y) = (`|x| * t, `|y| * t)}.
 Proof.
-rewrite -{-1}(subrK y x) => /(canLR (subrK _))/esym-Dx; rewrite Dx.
-by have [t ? [Dxy Dy]] := normC_add_eq Dx; exists t; rewrite // mulrDl -Dxy -Dy.
+set z := x - y; rewrite -(subrK y x) -/z => /(canLR (subrK _))/esym-Dx.
+have [t t_1 [Dz Dy]] := normC_add_eq Dx.
+by exists t; rewrite // Dx mulrDl -Dz -Dy.
 Qed.
 
 End ClosedFieldTheory.