diff options
| author | Cyril Cohen | 2020-09-29 20:44:05 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-29 20:44:05 +0200 |
| commit | 43538ace36aa9e5c4c999e24c418db09458b325b (patch) | |
| tree | 3098b37009bc40e5830e5cf571af6917cb369840 | |
| parent | d196c0953783d161e4b392ceac1ebf0ee9fe35dd (diff) | |
| parent | dad78be41d2852dd563333b69dc3f240056a95da (diff) | |
Merge pull request #506 from anton-trunov/ssrnat-extra-assoc-lemmas
ssrnat: add subnA, addnCB, addnCAC, addnAl lemmas
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 12 |
2 files changed, 13 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a8f6256..65c30cc 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -40,6 +40,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `finset.v`, new lemmas: `properC`, `properCr`, `properCl` - in `ssrnat.v`, new lemmas: `subn_minl`, `subn_maxl` - in `ssrnat.v`, new lemma: `oddS` +- in `ssrnat.v`, new lemmas: `subnA`, `addnBn`, `addnCAC`, `addnACl` - in `finset.v`, new lemmas: `mem_imset_eq`, `mem_imset2_eq`. These lemmas will lose the `_eq` suffix in the next release, when the shortende names will become availabe (cf. Renamed section) 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. |