proposition: Lemma splitPl x1 p x : x \in x1 :: p -> splitl x1 x p.
proof: Proof. rewrite inE; case: eqP => [->| _ /splitP[]]; first by rewrite -(cat0s p). by split; apply: last_rcons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)