diff options
| author | Laurent Théry | 2019-10-26 13:02:58 +0200 |
|---|---|---|
| committer | GitHub | 2019-10-26 13:02:58 +0200 |
| commit | 9ec6b02e673d0808b3ba4a6c4f849405bf222ae1 (patch) | |
| tree | 46671713f1ed295d65aca33ce957ba65b52743f0 /mathcomp | |
| parent | cd81418979c9783f9dae65d2aea98742919420e5 (diff) | |
| parent | 45b92eabb37cf1f8465ed2f3abe13666096c5c27 (diff) | |
Merge pull request #397 from CohenCyril/remove_addnKC
Removing duplicate lemma `addnKC` (= `addKn`)
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 5 |
1 files changed, 1 insertions, 4 deletions
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. |