proposition: Lemma eqseq_pivot2l x s1 s2 s3 s4 : x \notin s1 -> x \notin s3 -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
proof: Proof. move=> xNs1 xNs3; apply/idP/idP => [E|/andP[/eqP-> /eqP->]//]. suff S : size s1 = size s3 by rewrite eqseq_cat// eqseq_cons eqxx in E. by rewrite -(index_pivot s2 xNs1) (eqP E) index_pivot. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)