proposition: Lemma prefixP a b : reflect (exists s, a ++ s == b) (prefix a b).
proof: Proof. apply: (iffP idP); last by case=> s /eqP <-; exact: prefix_cat. elim: b a => [[] // _|h t IH]; first by exists [::]. case=> [/= _|x a]; first by exists (h :: t). rewrite prefix_cons => /andP[/eqP -> /IH[s Hs]]. by exists s; rewrite /= (eqP Hs). Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext