proposition: Lemma prefixE s1 s2 : prefix s1 s2 <-> exists s3, s2 = s1 ++ s3.
proof: Proof. split; last by case=>s3 ->; apply: prefix_cat. elim: s1 s2=>[|x xs IH] s2; first by exists s2. case: s2=>[/(_ 0 x erefl)//|y ys /prefix_cons' [?]]. by subst y=>/IH [s3 ->]; exists s3. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)