proposition: Lemma suffix_length_eq l1 l2 : l1 `suffix_of` l2 → length l2 ≤ length l1 → l1 = l2.
proof: Proof. intros. apply (inj reverse), prefix_length_eq. - by apply suffix_prefix_reverse. - by rewrite !reverse_length. Qed.
imports: stdpp(options)