proposition: Lemma infix_trans : transitive infix.
proof: Proof. move=> s s1 s2 /infixP[s1p [s1s def_s]] /infixP[sp [ss def_s2]]. by apply/infixP; exists (sp ++ s1p),(s1s ++ ss); rewrite def_s2 def_s -!catA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)