proposition: Lemma prefixW a b : a != b -> prefix a b -> size a < size b.
proof: Proof. move=> ab /prefixP[[|h t /eqP <-]]; first by rewrite cats0 (negbTE ab). by rewrite size_cat /= -addSnnS ltn_addr. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext