proposition: 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: Proof. 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. rewrite !filter_cat /= mem_cat inE eqxx orbT /=. rewrite uniq_eqseq_pivotl // => /andP [/eqP -> /eqP ->]. by rewrite !filter_subseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)