proposition: Lemma infix_catr s1 s2 s3 : infix s1 s2 -> infix s1 (s2 ++ s3).
proof: Proof. case: s3 => [|x s /infixP [p [sf]] ->]; first by rewrite cats0. by rewrite -catA; apply: infix_catl; rewrite -catA prefix_infix. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)