From b408b52bcb89468c7d61c4c56c2e7c02d8f458a8 Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Wed, 11 Nov 2020 20:32:54 +0100 Subject: make pivot the first argument in uniq_subseq_pivot Co-authored-by: Cyril Cohen --- mathcomp/ssreflect/seq.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 99405ec..a9ddb5e 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2382,10 +2382,10 @@ rewrite uniq_perm ?filter_uniq ?(subseq_uniq ss12) // => x. by rewrite mem_filter; apply: andb_idr; apply: (mem_subseq ss12). Qed. -Lemma uniq_subseq_pivot (s1 s2 s3 s4 : seq T) x (s := s3 ++ x :: s4) : +Lemma uniq_subseq_pivot x (s1 s2 s3 s4 : seq T) (s := s3 ++ x :: s4) : uniq s -> subseq (s1 ++ x :: s2) s = (subseq s1 s3 && subseq s2 s4). Proof. -move=> uniq_s; apply/idP/idP => [sub_s'_s|/andP[? ?]]; last first. +move=> uniq_s; apply/idP/idP => [sub_s'_s|/andP[? ?]]; last first. by rewrite cat_subseq //= eqxx. have uniq_s' := subseq_uniq sub_s'_s uniq_s. have/eqP {sub_s'_s uniq_s} := subseq_uniqP _ uniq_s sub_s'_s. -- cgit v1.2.3