# HG changeset patch
# User haftmann
# Date 1615446329 0
# Node ID 7b59d2945e546575ca2444cd2a03d0b4ca8de2fa
# Parent  fbd69f27769990eab503bb51792b4a501f119f81
lemma

diff -r fbd69f277699 -r 7b59d2945e54 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Thu Mar 11 11:22:25 2021 +0100
+++ b/src/HOL/Library/Permutations.thy	Thu Mar 11 07:05:29 2021 +0000
@@ -62,6 +62,10 @@
 lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> p permutes T"
   unfolding permutes_def by blast
 
+lemma permutes_imp_permutes_insert:
+  \<open>p permutes insert x S\<close> if \<open>p permutes S\<close>
+  using that by (rule permutes_subset) auto
+
 lemma permutes_empty[simp]: "p permutes {} \<longleftrightarrow> p = id"
   by (auto simp add: fun_eq_iff permutes_def)