diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 9 |
1 files changed, 9 insertions, 0 deletions
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. |