diff options
| author | Cyril Cohen | 2019-10-25 19:08:56 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-10-25 19:10:18 +0200 |
| commit | 45b92eabb37cf1f8465ed2f3abe13666096c5c27 (patch) | |
| tree | 46671713f1ed295d65aca33ce957ba65b52743f0 | |
| parent | cd81418979c9783f9dae65d2aea98742919420e5 (diff) | |
Removing duplicate lemma `addnKC` (= `addKn`)
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 5 |
2 files changed, 3 insertions, 6 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3737972..50ad28a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -35,8 +35,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: `addnKC`, `ltn_predl`, - `ltn_predr`, `ltn_subr` and `predn_sub`, + - some trivial results in ssrnat: `ltn_predl`, `ltn_predr`, + `ltn_subr` 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 diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 746eafc..39131f0 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -279,9 +279,6 @@ Proof. by move=> m; rewrite /= -{2}[n]addn0 subnDl subn0. Qed. Lemma addnK n : cancel (addn^~ n) (subn^~ n). Proof. by move=> m; rewrite /= (addnC m) addKn. Qed. -Lemma addnKC n m : (n + m) - n = m. -Proof. by rewrite addnC addnK. Qed. - Lemma subSnn n : n.+1 - n = 1. Proof. exact (addnK n 1). Qed. @@ -542,7 +539,7 @@ Lemma subnBA m n p : p <= n -> m - (n - p) = m + p - n. Proof. by move=> le_pn; rewrite -{2}(subnK le_pn) subnDr. Qed. Lemma ltn_subr m n : m <= n -> (n - m < n) = (m > 0). -Proof. by move=> le_mn; rewrite -subn_gt0 subnBA// addnKC. Qed. +Proof. by move=> le_mn; rewrite -subn_gt0 subnBA// addKn. Qed. Lemma subKn m n : m <= n -> n - (n - m) = m. Proof. by move/subnBA->; rewrite addKn. Qed. |