proposition: Lemma prefix_suffix_trans s2 s1 s3 : prefix s1 s2 -> suffix s2 s3 -> infix s1 s3.
proof: Proof. by move=> /prefixW + /suffixW +; apply: infix_trans. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)