[STATEMENT]
lemma mult1I:
  assumes "M = add_mset a M0" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
  shows "(N, M) \<in> mult1 r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (N, M) \<in> mult1 r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
M = add_mset a M0
N = M0 + K
?b \<in># K \<Longrightarrow> (?b, a) \<in> r

goal (1 subgoal):
 1. (N, M) \<in> mult1 r
[PROOF STEP]
unfolding mult1_def
[PROOF STATE]
proof (prove)
using this:
M = add_mset a M0
N = M0 + K
?b \<in># K \<Longrightarrow> (?b, a) \<in> r

goal (1 subgoal):
 1. (N, M) \<in> {(N, M). \<exists>a M0 K. M = add_mset a M0 \<and> N = M0 + K \<and> (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r)}
[PROOF STEP]
by blast