proposition: Lemma prefixP {s1 s2} : reflect (exists s2' : seq T, s2 = s1 ++ s2') (prefix s1 s2).
proof: Proof. apply: (iffP idP) => [|[{}s2 ->]]; last exact: prefix_prefix. by rewrite prefixE => /eqP<-; exists (drop (size s1) s2); rewrite cat_take_drop. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)