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.

1 files changed, 1 insertions, 1 deletions

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.