proposition: Lemma infixPn s1 s2 : reflect (infix_index s1 s2 = (size s2).+1) (~~ infix s1 s2).
proof: Proof. rewrite -infixTindex -ltnNge; apply: (iffP idP) => [s2lt|->//]. by apply/eqP; rewrite eqn_leq s2lt infix_index_le. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)