proposition: Lemma eqseq_pivotl x s1 s2 s3 s4 : x \notin s1 -> x \notin s2 -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
proof: Proof. move=> xNs1 xNs2; apply/idP/idP => [E|/andP[/eqP-> /eqP->]//]. rewrite -(@eqseq_pivot2l x)//; have /eqP/(congr1 (count_mem x)) := E. rewrite !count_cat/= eqxx !addnS (count_memPn _ _ xNs1) (count_memPn _ _ xNs2). by move=> -[/esym/eqP]; rewrite addn_eq0 => /andP[/eqP/count_memPn]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)