From 74d21e0173df1e084e1e78fe0285036633aed94b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 14 Jan 2022 13:47:56 +0100
Subject: [PATCH] Move `elem_of_suffix` to other suffix lemmas.

---
 theories/list.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index b6a72eac..77477011 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2078,9 +2078,6 @@ Proof. intros [??]. discriminate_list. Qed.
 Lemma elem_of_prefix l1 l2 x :
   x ∈ l1 → l1 `prefix_of` l2 → x ∈ l2.
 Proof. intros Hin [l' ->]. apply elem_of_app. by left. Qed.
-Lemma elem_of_suffix l1 l2 x :
-  x ∈ l1 → l1 `suffix_of` l2 → x ∈ l2.
-Proof. intros Hin [l' ->]. apply elem_of_app. by right. Qed.
 (* [prefix] is not a total order, but [l1] and [l2] are always comparable if
   they are both prefixes of some [l3]. *)
 Lemma prefix_weak_total l1 l2 l3 :
@@ -2230,6 +2227,9 @@ Lemma suffix_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
 Proof. intros [? ->]. rewrite app_length. lia. Qed.
 Lemma suffix_cons_not x l : ¬x :: l `suffix_of` l.
 Proof. intros [??]. discriminate_list. Qed.
+Lemma elem_of_suffix l1 l2 x :
+  x ∈ l1 → l1 `suffix_of` l2 → x ∈ l2.
+Proof. intros Hin [l' ->]. apply elem_of_app. by right. Qed.
 (* [suffix] is not a total order, but [l1] and [l2] are always comparable if
   they are both suffixes of some [l3]. *)
 Lemma suffix_weak_total l1 l2 l3 :
-- 
GitLab