proposition: Lemma prefix_suffix_reverse l1 l2 : l1 `prefix_of` l2 ↔ reverse l1 `suffix_of` reverse l2.
proof: Proof. split; intros [k E]; exists (reverse k). - by rewrite E, reverse_app. - by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive. Qed.
imports: stdpp(options)