proposition: Lemma prefix_common a b s : prefix a s -> prefix b s -> prefix a b \/ prefix b a.
proof: Proof. case/prefixP => t /eqP <-{s} /prefixP[t']. wlog : t t' a b / size a <= size b. move=> H. case/boolP : (size a <= size b) => [? K|]; first exact: (H t t'). rewrite leqNgt negbK => /ltnW /(H t' t) {}H /eqP/esym/eqP; tauto. move=> ab H; left; apply/prefixP; exists (take (size b - size a) t). move/eqP : H => /(congr1 (take (size b))). by rewrite take_cat ltnn subnn take0 cats0 take_cat ltnNge ab /= => <-. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext