proposition: Lemma suffixE s1 s2 : suffix s1 s2 = (drop (size s2 - size s1) s2 == s1).
proof: Proof. by rewrite /suffix prefixE take_rev (can_eq revK) size_rev. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)