proposition: Lemma prefix_catr s1 s2 s1' s3 : size s1 = size s1' -> prefix (s1 ++ s2) (s1' ++ s3) = (s1 == s1') && prefix s2 s3.
proof: Proof. elim: s1 s1' => [|x s1 IHs1] [|y s1']//= [eqs1]. by rewrite IHs1// eqseq_cons andbA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)