proposition: Lemma prefix_size (s t : seq A) : prefix s t -> size s <= size t.
proof: Proof. elim: s t=>[//|a s IH] [|b t] H; first by move: (H 0 a (erefl _)). by rewrite ltnS; apply: (IH _ (proj2 (prefix_cons' H))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq)