diff options
| author | Cyril Cohen | 2020-06-24 18:24:15 +0200 |
|---|---|---|
| committer | GitHub | 2020-06-24 18:24:15 +0200 |
| commit | 3728862662bd0a5b836dfa746921954604d051ec (patch) | |
| tree | 605d0a0e4bceb7335ccb6c97ebf9c2e84c7f8331 /mathcomp | |
| parent | 85c876ba8db646af6258445ee6838b184eaaedb3 (diff) | |
| parent | d5aba2075565dd855c15b73e01a3c34f8f9b2313 (diff) | |
Merge pull request #540 from thery/doc
fix the doc for ubnP in ssrnat
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 6 |
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 *) |