diff options
| author | Cyril Cohen | 2021-01-18 19:40:30 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2021-01-19 03:02:09 +0100 |
| commit | 1b1b52fc8777c54f411c8c51dc9ce5d4dbf137a8 (patch) | |
| tree | 6dc1b8e2ad61445b157e826059c208e5455138a7 /CHANGELOG_UNRELEASED.md | |
| parent | 35fc6b309a5cc87570255addfd135cb4650ebb43 (diff) | |
Adding lemma sumnB
cf https://stackoverflow.com/questions/61556710
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1e779c3..839e796 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,6 +10,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Added +- in `ssrnat.v`, added lemma `sumnB`. + - in `seq.v`, + new higher-order predicate `pairwise r xs` which asserts that the relation `r` holds for any i-th and j-th element of `xs` such that i < j. |