proposition: Lemma prefix_size s1 s2 : prefix s1 s2 -> size s1 <= size s2.
proof: Proof. elim: s1 s2=>[//|a s1 IH] [|b s2] H; first by move: (H 0 a (erefl _)). by rewrite ltnS; apply: (IH _ (proj2 (prefix_cons' H))). 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)