From 7ea7cd6ef399cdb8ed4eb25485cde1a4d604943f Mon Sep 17 00:00:00 2001
From: Florent Hivert
Date: Tue, 3 Sep 2019 23:06:46 +0200
Subject: More lemmas on seqs

---
 CHANGELOG_UNRELEASED.md | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'CHANGELOG_UNRELEASED.md')

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 28d1b5c..9a14eec 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -85,6 +85,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Added lemmas on commutation with difference, big sum and prod:
   `commrB`, `commr_sum`, `commr_prod`.
 
+- Added a few basic seq lemmas about `nseq`, `take` and `drop`:
+  `nseq_addn`, `take_take`, `take_drop`, `take_addn`, `takeC`,
+  `take_nseq`, `drop_nseq`, `rev_nseq`, `take_iota`, `drop_iota`.
+
+
 ### Changed
 
 - `eqVneq` lemma is changed from `{x = y} + {x != y}` to
-- 
cgit v1.2.3