[STATEMENT]
lemma iMOD_div: "
  \<lbrakk> 0 < k; m mod k = 0 \<rbrakk> \<Longrightarrow>
  [r, mod m] \<oslash> k = [r div k, mod (m div k) ]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; m mod k = 0\<rbrakk> \<Longrightarrow> [ r, mod m ] \<oslash> k = [ r div k, mod m div k ]
[PROOF STEP]
apply (case_tac "m = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < k; m mod k = 0; m = 0\<rbrakk> \<Longrightarrow> [ r, mod m ] \<oslash> k = [ r div k, mod m div k ]
 2. \<lbrakk>0 < k; m mod k = 0; m \<noteq> 0\<rbrakk> \<Longrightarrow> [ r, mod m ] \<oslash> k = [ r div k, mod m div k ]
[PROOF STEP]
apply (simp add: iMOD_0 iIN_0 iT_Div_singleton)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; m mod k = 0; m \<noteq> 0\<rbrakk> \<Longrightarrow> [ r, mod m ] \<oslash> k = [ r div k, mod m div k ]
[PROOF STEP]
apply (clarsimp elim!: dvdE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ka. \<lbrakk>0 < k; 0 < ka; m = k * ka\<rbrakk> \<Longrightarrow> [ r, mod k * ka ] \<oslash> k = [ r div k, mod ka ]
[PROOF STEP]
apply (rename_tac q)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; m = k * q\<rbrakk> \<Longrightarrow> [ r, mod k * q ] \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply hypsubst_thin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q\<rbrakk> \<Longrightarrow> [ r, mod k * q ] \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (cut_tac r="r div k" and k=k and m=q in iMOD_mult)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r div k, mod q ] \<otimes> k = [ r div k * k, mod q * k ]\<rbrakk> \<Longrightarrow> [ r, mod k * q ] \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (drule arg_cong[where f="\<lambda>x. x \<oplus> (r mod k)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r div k, mod q ] \<otimes> k \<oplus> r mod k = [ r div k * k, mod q * k ] \<oplus> r mod k\<rbrakk> \<Longrightarrow> [ r, mod k * q ] \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r div k * k, mod q * k ] \<oplus> r mod k = [ r div k, mod q ] \<otimes> k \<oplus> r mod k\<rbrakk> \<Longrightarrow> [ r, mod k * q ] \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (simp add: iMOD_add mult.commute[of k])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (cut_tac I="[r div k, mod q] \<otimes> k" and m=k and n="r mod k" in iT_Plus_Div_distrib_mod_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k\<rbrakk> \<Longrightarrow> \<forall>x\<in>[ r div k, mod q ] \<otimes> k. x mod k + r mod k mod k < k
 2. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ] \<otimes> k \<oslash> k \<oplus> r mod k div k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q x. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; x \<in> [ r div k, mod q ] \<otimes> k\<rbrakk> \<Longrightarrow> x mod k + r mod k mod k < k
 2. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ] \<otimes> k \<oslash> k \<oplus> r mod k div k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (simp only: iMOD_mult iMOD_iff, elim conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q x. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k * k, mod q * k ] \<oplus> r mod k; x mod (q * k) = r div k * k mod (q * k); r div k * k \<le> x\<rbrakk> \<Longrightarrow> x mod k + r mod k mod k < k
 2. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ] \<otimes> k \<oslash> k \<oplus> r mod k div k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (drule mod_factor_imp_mod_0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q x. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k * k, mod q * k ] \<oplus> r mod k; r div k * k \<le> x; x mod k = 0\<rbrakk> \<Longrightarrow> x mod k + r mod k mod k < k
 2. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ] \<otimes> k \<oslash> k \<oplus> r mod k div k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ] \<otimes> k \<oslash> k \<oplus> r mod k div k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (simp add: iT_Plus_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ] \<otimes> k \<oslash> k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (simp add: iT_Mult_Div[OF _ mod_self] iT_Mult_1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done