proposition: Lemma suffix_catl s1 s2 s3 s3' : size s3 = size s3' -> suffix (s1 ++ s3) (s2 ++ s3') = (s3 == s3') && suffix s1 s2.
proof: Proof. by move=> eqs3; rewrite /suffix !rev_cat prefix_catr ?size_rev// (can_eq revK). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)