From 2acb66dcb2d8e571b3edfecf70099893187a169f Mon Sep 17 00:00:00 2001
From: Christian Doczkal
Date: Fri, 6 Nov 2020 20:41:52 +0100
Subject: fixup after feedback from Cyril

---
 CHANGELOG_UNRELEASED.md  | 4 ++++
 mathcomp/ssreflect/seq.v | 9 +++++----
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index ecf539a..c635497 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -272,6 +272,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - in `seq.v` new lemmas `eqseq_pivot`, `eqseq_pivot_uniql`, `eqseq_pivot_uniqr`,
   `mask_rcons, `rev_mask`, `subseq_rev`, `subseq_cat2l`, `subseq_cat2r`, `subseq_rot`, and
+- in `seq.v` new lemmas `index_pivot`, `take_pivot`, `rev_pivot`,
+  `eqseq_pivot2l`, `eqseq_pivot2r`, `eqseq_pivotl`, `eqseq_pivotr`
+  `uniq_eqseq_pivotl`, `uniq_eqseq_pivotr`, `mask_rcons, `rev_mask`,
+  `subseq_rev`, `subseq_cat2l`, `subseq_cat2r`, `subseq_rot`, and
   `uniq_subseq_pivot`.
 
 ### Changed
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 16f17c3..a85ff76 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1395,12 +1395,13 @@ Proof. by move=> x; rewrite -[s in RHS](cat_take_drop n0) !mem_cat /= orbC. Qed.
 Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2).
 Proof. exact/inj_eq/rot_inj. Qed.
 
+(* lemmas about the pivot pattern [_ ++ _ :: _] *)
 
-Lemma index_pivot x s1 s2 (s := s1 ++ x :: s2) : x \notin s1 -> 
+Lemma index_pivot x s1 s2 (s := s1 ++ x :: s2) : x \notin s1 ->
   index x s = size s1.
 Proof. by rewrite index_cat/= eqxx addn0; case: ifPn. Qed.
 
-Lemma take_pivot x s2 s1 (s := s1 ++ x :: s2) : x \notin s1 -> 
+Lemma take_pivot x s2 s1 (s := s1 ++ x :: s2) : x \notin s1 ->
   take (index x s) s = s1.
 Proof. by move=> /index_pivot->; rewrite take_size_cat. Qed.
 
@@ -1419,7 +1420,7 @@ Lemma eqseq_pivot2r x s1 s2 s3 s4 : x \notin s2 -> x \notin s4 ->
   (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
 Proof.
 move=> xNs2 xNs4; rewrite -(can_eq revK) !rev_pivot.
-by rewrite eqseq_pivot2l ?mem_rev// !(can_eq revK) andbC.
+by rewrite eqseq_pivot2l ?mem_rev // !(can_eq revK) andbC.
 Qed.
 
 Lemma eqseq_pivotl x s1 s2 s3 s4 : x \notin s1 -> x \notin s2 ->
@@ -2394,7 +2395,7 @@ Proof.
 move => uniq_s sub_s'_s; have uniq_s' := subseq_uniq sub_s'_s uniq_s.
 have/eqP {sub_s'_s uniq_s} := subseq_uniqP _ uniq_s sub_s'_s.
 rewrite !filter_cat /= mem_cat inE eqxx orbT /=.
-rewrite eqseq_pivot_uniql // => /andP [/eqP -> /eqP ->].
+rewrite uniq_eqseq_pivotl // => /andP [/eqP -> /eqP ->].
 by rewrite !filter_subseq.
 Qed.
 
-- 
cgit v1.2.3