[STATEMENT]
lemma mono_multp[mono]: "r \<le> r' \<Longrightarrow> multp r \<le> multp r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> r' \<Longrightarrow> multp r \<le> multp r'
[PROOF STEP]
unfolding le_fun_def le_bool_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x xa. r x xa \<longrightarrow> r' x xa \<Longrightarrow> \<forall>x xa. multp r x xa \<longrightarrow> multp r' x xa
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>x xa. r x xa \<longrightarrow> r' x xa; multp r x xa\<rbrakk> \<Longrightarrow> multp r' x xa
[PROOF STEP]
fix M N :: "'a multiset"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>x xa. r x xa \<longrightarrow> r' x xa; multp r x xa\<rbrakk> \<Longrightarrow> multp r' x xa
[PROOF STEP]
assume "\<forall>x xa. r x xa \<longrightarrow> r' x xa"
[PROOF STATE]
proof (state)
this:
\<forall>x xa. r x xa \<longrightarrow> r' x xa

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>x xa. r x xa \<longrightarrow> r' x xa; multp r x xa\<rbrakk> \<Longrightarrow> multp r' x xa
[PROOF STEP]
hence "{(x, y). r x y} \<subseteq> {(x, y). r' x y}"
[PROOF STATE]
proof (prove)
using this:
\<forall>x xa. r x xa \<longrightarrow> r' x xa

goal (1 subgoal):
 1. {(x, y). r x y} \<subseteq> {(x, y). r' x y}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{(x, y). r x y} \<subseteq> {(x, y). r' x y}

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>x xa. r x xa \<longrightarrow> r' x xa; multp r x xa\<rbrakk> \<Longrightarrow> multp r' x xa
[PROOF STEP]
thus "multp r M N \<Longrightarrow> multp r' M N"
[PROOF STATE]
proof (prove)
using this:
{(x, y). r x y} \<subseteq> {(x, y). r' x y}

goal (1 subgoal):
 1. multp r M N \<Longrightarrow> multp r' M N
[PROOF STEP]
unfolding multp_def
[PROOF STATE]
proof (prove)
using this:
{(x, y). r x y} \<subseteq> {(x, y). r' x y}

goal (1 subgoal):
 1. (M, N) \<in> mult {(x, y). r x y} \<Longrightarrow> (M, N) \<in> mult {(x, y). r' x y}
[PROOF STEP]
by (fact mono_mult[THEN subsetD, rotated])
[PROOF STATE]
proof (state)
this:
multp r M N \<Longrightarrow> multp r' M N

goal:
No subgoals!
[PROOF STEP]
qed