From 664feb54237e18e7a1528321bdd8fd28d1e0f1be Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Tue, 24 Jul 2018 17:10:22 +0200
Subject: Add addnBAC, addnBCA, and addnABC lemmas to ssrnat

Proofs by Cyril Cohen
---
 mathcomp/ssreflect/ssrnat.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 4619db7..b7ff16c 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -512,6 +512,15 @@ Proof. by rewrite addnC; apply: subnKC. Qed.
 Lemma addnBA m n p : p <= n -> m + (n - p) = m + n - p.
 Proof. by move=> le_pn; rewrite -{2}(subnK le_pn) addnA addnK. Qed.
 
+Lemma addnBAC m n p : n <= m -> m - n + p = m + p - n.
+Proof. by move=> le_nm; rewrite addnC addnBA // addnC. Qed.
+
+Lemma addnBCA m n p : p <= m -> p <= n -> m + (n - p) = n + (m - p).
+Proof. by move=> le_pm le_pn; rewrite !addnBA // addnC. Qed.
+
+Lemma addnABC m n p : p <= m -> p <= n -> m + (n - p) = m - p + n.
+Proof. by move=> le_pm le_pn; rewrite addnBA // addnBAC. Qed.
+
 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.
 
-- 
cgit v1.2.3