proposition: Lemma infixTindex s1 s2 : (infix_index s1 s2 <= size s2) = infix s1 s2.
proof: Proof. by elim: s2 s1 => [|y s2 +] [|x s1]//= => <-; case: ifP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)