proposition: Lemma infixE s1 s2 : infix s1 s2 = (take (size s1) (drop (infix_index s1 s2) s2) == s1).
proof: Proof. elim: s2 s1 => [|y s2 +] [|x s1]//= => -> /=. by case: ifP => // /andP[/eqP-> ps1s2/=]; rewrite eqseq_cons -prefixE eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)