diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 45a0cc67c8a0ec769052f38eb5f7f1a83cfda162..1d1dd5ca962655cecec59d12a6e8344728039218 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -938,7 +938,7 @@ Qed.
 Lemma map_to_list_singleton {A} i (x : A) :
   map_to_list ({[i:=x]} : M A) = [(i,x)].
 Proof.
-  apply Permutation_singleton. unfold singletonM, map_singleton.
+  apply Permutation_singleton_r. unfold singletonM, map_singleton.
   by rewrite map_to_list_insert, map_to_list_empty by eauto using lookup_empty.
 Qed.
 Lemma map_to_list_delete {A} (m : M A) i x :
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 21b71cc63eb923230b0ba956f20b074476529bbf..a458157121d40b54685db6761521bf9d3c5690f3 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -85,7 +85,7 @@ Qed.
 Lemma elements_empty' X : elements X = [] ↔ X ≡ ∅.
 Proof.
   split; intros HX; [by apply elements_empty_inv|].
-  by rewrite <-Permutation_nil, HX, elements_empty.
+  by rewrite <-Permutation_nil_r, HX, elements_empty.
 Qed.
 
 Lemma elements_union_singleton (X : C) x :
@@ -99,7 +99,7 @@ Proof.
 Qed.
 Lemma elements_singleton x : elements ({[ x ]} : C) = [x].
 Proof.
-  apply Permutation_singleton. by rewrite <-(right_id ∅ (∪) {[x]}),
+  apply Permutation_singleton_r. by rewrite <-(right_id ∅ (∪) {[x]}),
     elements_union_singleton, elements_empty by set_solver.
 Qed.
 Lemma elements_disj_union (X Y : C) :
diff --git a/theories/list.v b/theories/list.v
index deb74608d21aef708c806219dad068d82530c898..1f8f5ed0ffd8af0cc37c93ff3bc5b41ba7e4b5b9 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1692,10 +1692,14 @@ Proof.
 Qed.
 
 (** ** Properties of the [Permutation] predicate *)
-Lemma Permutation_nil l : l ≡ₚ [] ↔ l = [].
+Lemma Permutation_nil_r l : l ≡ₚ [] ↔ l = [].
 Proof. split; [by intro; apply Permutation_nil | by intros ->]. Qed.
-Lemma Permutation_singleton l x : l ≡ₚ [x] ↔ l = [x].
+Lemma Permutation_singleton_r l x : l ≡ₚ [x] ↔ l = [x].
 Proof. split; [by intro; apply Permutation_length_1_inv | by intros ->]. Qed.
+Lemma Permutation_nil_l l : [] ≡ₚ l ↔ [] = l.
+Proof. by rewrite (symmetry_iff (≡ₚ)), Permutation_nil_r. Qed.
+Lemma Permutation_singleton_l l x : [x] ≡ₚ l ↔ [x] = l.
+Proof. by rewrite (symmetry_iff (≡ₚ)), Permutation_singleton_r. Qed.
 
 Lemma Permutation_skip x l l' : l ≡ₚ l' → x :: l ≡ₚ x :: l'.
 Proof. apply perm_skip. Qed.
@@ -1762,7 +1766,7 @@ Proof.
   - intros [k ->]. by left.
 Qed.
 
-Lemma Permutation_cons_inv l k x :
+Lemma Permutation_cons_inv_r l k x :
   k ≡ₚ x :: l → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
 Proof.
   intros Hk. assert (∃ i, k !! i = Some x) as [i Hi].
@@ -1772,6 +1776,9 @@ Proof.
   - rewrite <-delete_take_drop. apply (inj (x ::.)).
     by rewrite <-Hk, <-(delete_Permutation k) by done.
 Qed.
+Lemma Permutation_cons_inv_l l k x :
+  x :: l ≡ₚ k → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
+Proof. by intros ?%(symmetry_iff (≡ₚ))%Permutation_cons_inv_r. Qed.
 
 Lemma Permutation_cross_split l la lb lc ld :
   la ++ lb ≡ₚ l →
diff --git a/theories/sorting.v b/theories/sorting.v
index 3f019e54d0e6902b2a0de8d23074b656831b0621..afd9da0b1ba3858477cf3fc3a7ccfa29d84353ae 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -77,7 +77,7 @@ Section sorted.
     intros Hl1; revert l2. induction Hl1 as [|x1 l1 ? IH Hx1]; intros l2 Hl2 E.
     { symmetry. by apply Permutation_nil. }
     destruct Hl2 as [|x2 l2 ? Hx2].
-    { by apply Permutation_nil in E. }
+    { by apply Permutation_nil_r in E. }
     assert (x1 = x2); subst.
     { rewrite Forall_forall in Hx1, Hx2.
       assert (x2 ∈ x1 :: l1) as Hx2' by (by rewrite E; left).