[STATEMENT]
lemma add_eq_conv_ex:
  "(add_mset a M = add_mset b N) =
    (M = N \<and> a = b \<or> (\<exists>K. M = add_mset b K \<and> N = add_mset a K))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (add_mset a M = add_mset b N) = (M = N \<and> a = b \<or> (\<exists>K. M = add_mset b K \<and> N = add_mset a K))
[PROOF STEP]
by (auto simp add: add_eq_conv_diff)