proposition: Lemma infixW s1 s2 : infix s1 s2 -> subseq s1 s2.
proof: Proof. move=> /infixP[sp [ss ->]]. exact: subseq_trans (prefix_subseq _ _) (suffix_subseq _ _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)