From dad78be41d2852dd563333b69dc3f240056a95da Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Wed, 13 May 2020 17:11:30 +0300
Subject: ssrnat: add subnA, addnCB, addnCAC, addnAl lemmas

---
 mathcomp/ssreflect/ssrnat.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 7a996d1..8b88821 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -222,6 +222,12 @@ Proof. by move=> m n p; rewrite (addnC n) addnCA addnC. Qed.
 Lemma addnAC : right_commutative addn.
 Proof. by move=> m n p; rewrite -!addnA (addnC n). Qed.
 
+Lemma addnCAC m n p : m + n + p = p + n + m.
+Proof. by rewrite addnC addnA addnAC. Qed.
+
+Lemma addnACl m n p: m + n + p = n + (p + m).
+Proof. by rewrite (addnC m) addnC addnCA. Qed.
+
 Lemma addnACA : interchange addn addn.
 Proof. by move=> m n p q; rewrite -!addnA (addnCA n). Qed.
 
@@ -530,6 +536,9 @@ Proof. by rewrite ltnNge leq_subrR negb_or !lt0n. Qed.
 Lemma subnKC m n : m <= n -> m + (n - m) = n.
 Proof. by elim: m n => [|m IHm] [|n] // /(IHm n) {2}<-. Qed.
 
+Lemma addnBn m n : m + (n - m) = m - n + n.
+Proof. by elim: m n => [|m IHm] [|n] //; rewrite addSn addnS IHm. Qed.
+
 Lemma subnK m n : m <= n -> (n - m) + m = n.
 Proof. by rewrite addnC; apply: subnKC. Qed.
 
@@ -548,6 +557,9 @@ 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 -[in RHS](subnK le_pn) subnDr. Qed.
 
+Lemma subnA m n p : p <= n -> n <= m -> m - (n - p) = m - n + p.
+Proof. by move=> le_pn lr_nm; rewrite addnBAC // subnBA. Qed.
+
 Lemma subKn m n : m <= n -> n - (n - m) = m.
 Proof. by move/subnBA->; rewrite addKn. Qed.
 
-- 
cgit v1.2.3