From 45b92eabb37cf1f8465ed2f3abe13666096c5c27 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 25 Oct 2019 19:08:56 +0200
Subject: Removing duplicate lemma `addnKC` (= `addKn`)

---
 mathcomp/ssreflect/ssrnat.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'mathcomp')

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.
-- 
cgit v1.2.3