proposition: Lemma infixP {s1 s2} : reflect (exists s s' : seq T, s2 = s ++ s1 ++ s') (infix s1 s2).
proof: Proof. apply: (iffP idP) => [|[p [s {s2}->]]]//=; rewrite infixE => /eqP<-. set k := infix_index _ _; exists (take k s2), (drop (size s1 + k) s2). by rewrite -drop_drop !cat_take_drop. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)