fix the doc for ubnP in ssrnat

1 files changed, 3 insertions, 3 deletions

diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 39c8451..6837eb1 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -403,7 +403,7 @@ 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 ... *.    *)
+(*   have [n 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                                                                   *)
@@ -416,11 +416,11 @@ Proof. by rewrite -implyNb -ltnNge; apply/implyP; apply: ltnW. Qed.
 (*  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.   *)
+(*   have [n] := 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 ... *.  *)
+(*  have [n 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                          *)