proposition: Lemma prefix_cat s1 s2 : prefix s1 (s1 ++ s2).
proof: Proof. elim: s2 s1=>[|x xs IH] s1; first by rewrite cats0. rewrite -cat_rcons; apply: prefix_trans (IH _). by apply: prefix_rcons. 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)