diff options
| author | Cyril Cohen | 2019-11-18 15:39:33 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-11-18 15:39:33 +0100 |
| commit | 95e69d88e9f629c043939b8315e73dbb58852d9a (patch) | |
| tree | 7c231baedeb8cda341785757f412bf65f4d0bbeb | |
| parent | 359abfc1d67843216b0362d2fee3b8d650ff7ec0 (diff) | |
fixing CHANGELOG and ltn_pred lemmas
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 4 |
2 files changed, 4 insertions, 6 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 69f53ea..f0d9719 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -36,8 +36,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `big_enum_val`, `big_enum_rank`, `big_set`. - Arithmetic theorems in ssrnat and div: - - some trivial results in ssrnat: `ltn_predl`, `ltn_predr`, - `ltn_subr`, `leq_subl`, `ltn_subl` and `predn_sub`, + - some trivial results in ssrnat: `ltn_predL`, `ltn_predRL`, + `ltn_subrR`, `leq_subrR`, `ltn_subrL` and `predn_sub`, - theorems about `n <=/< p +/- m` and `m +/- n <=/< p`: `leq_psubRL`, `ltn_psubLR`, `leq_subRL`, `ltn_subLR`, `leq_subCl`, `leq_psubCr`, `leq_subCr`, `ltn_subCr`, `ltn_psubCl` and @@ -119,8 +119,6 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `ssrnat.mc_1_9` module. One may compile proofs compatible with the version 1.9 in newer versions by using this module. -- `leq_subr` has been renamed `leq_subl` (and the latter has been reallocated) - ### Removed - `fin_inj_bij` lemma is removed as a duplicate of `injF_bij` lemma diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 6e54a55..d47a3ba 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -326,10 +326,10 @@ Hint Resolve leqnSn : core. Lemma leq_pred n : n.-1 <= n. Proof. by case: n => /=. Qed. Lemma leqSpred n : n <= n.-1.+1. Proof. by case: n => /=. Qed. -Lemma ltn_predl n : (n.-1 < n) = (0 < n). +Lemma ltn_predL n : (n.-1 < n) = (0 < n). Proof. by case: n => [//|n]; rewrite ltnSn. Qed. -Lemma ltn_predr m n : (m < n.-1) = (m.+1 < n). +Lemma ltn_predRL m n : (m < n.-1) = (m.+1 < n). Proof. by case: n => [//|n]; rewrite succnK. Qed. Lemma ltn_predK m n : m < n -> n.-1.+1 = n. |