proposition: Lemma suffixP {s1 s2} : reflect (exists s2' : seq T, s2 = s2' ++ s1) (suffix s1 s2).
proof: Proof. apply: (iffP prefixP) => [[s2' rev_s2]|[s2' ->]]; exists (rev s2'); last first. by rewrite rev_cat. by rewrite -[s2]revK rev_s2 rev_cat revK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)