proposition: Lemma infix_rev s1 s2 : infix (rev s1) (rev s2) = infix s1 s2.
proof: Proof. gen have sr : s1 s2 / infix s1 s2 -> infix (rev s1) (rev s2); last first. by apply/idP/idP => /sr; rewrite ?revK. by move=> /infixP[s [p ->]]; rewrite !rev_cat -catA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)