make pivot the first argument in uniq_subseq_pivot

Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>

1 files changed, 2 insertions, 2 deletions

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.