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