892 lemma plus_perm_eq:

   893   fixes p q::"perm"

   894   assumes asm: "supp p \<inter>  supp q = {}"

   895   shows "p + q  = q + p"

   896 unfolding expand_perm_eq

   897 proof

   898   fix a::"atom"

   899   show "(p + q) \<bullet> a = (q + p) \<bullet> a"

   900   proof -

   901     { assume "a \<notin> supp p" "a \<notin> supp q"

   902       then have "(p + q) \<bullet> a = (q + p) \<bullet> a" 

   903 	by (simp add: supp_perm)

   904     }

   905     moreover

   906     { assume a: "a \<in> supp p" "a \<notin> supp q"

   907       then have "p \<bullet> a \<in> supp p" by (simp add: supp_perm)

   908       then have "p \<bullet> a \<notin> supp q" using asm by auto

   909       with a have "(p + q) \<bullet> a = (q + p) \<bullet> a" 

   910 	by (simp add: supp_perm)

   911     }

   912     moreover

   913     { assume a: "a \<notin> supp p" "a \<in> supp q"

   914       then have "q \<bullet> a \<in> supp q" by (simp add: supp_perm)

   915       then have "q \<bullet> a \<notin> supp p" using asm by auto 

   916       with a have "(p + q) \<bullet> a = (q + p) \<bullet> a" 

   917 	by (simp add: supp_perm)

   918     }

   919     ultimately show "(p + q) \<bullet> a = (q + p) \<bullet> a" 

   920       using asm by blast

   921   qed

   922 qed