proposition: Lemma suffix_rcons s1 s2 x y : suffix (rcons s1 x) (rcons s2 y) = (x == y) && suffix s1 s2.
proof: Proof. by rewrite /suffix 2!rev_rcons prefix_cons. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)