[STATEMENT]
lemma "((x::nat) div y) div z = (x div (y*z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x div y div z = x div (y * z)
[PROOF STEP]
using div_mult2_eq
[PROOF STATE]
proof (prove)
using this:
?m div (?n * ?q) = ?m div ?n div ?q

goal (1 subgoal):
 1. x div y div z = x div (y * z)
[PROOF STEP]
by auto


[STATEMENT]
lemma "(\<not>((a::nat) < b)) \<Longrightarrow> (a \<ge> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> a < b \<Longrightarrow> b \<le> a
[PROOF STEP]
by auto


[STATEMENT]
lemma not_null: "xs \<noteq> [] \<Longrightarrow> \<exists>y ys. xs = y#ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> \<exists>y ys. xs = y # ys
[PROOF STEP]
by (metis neq_Nil_conv)


[STATEMENT]
lemma "(y::nat) \<noteq> 0 \<Longrightarrow> (x mod y) < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<noteq> 0 \<Longrightarrow> x mod y < y
[PROOF STEP]
using mod_less_divisor
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> ?m mod ?n < ?n

goal (1 subgoal):
 1. y \<noteq> 0 \<Longrightarrow> x mod y < y
[PROOF STEP]
by auto


[STATEMENT]
lemma mod_prop1:"((a::nat) mod (b*c)) mod c = (a mod c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod (b * c) mod c = a mod c
[PROOF STEP]
proof(cases "c = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
 2. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
 2. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
have "b*c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * c = 0
[PROOF STEP]
by (metis True mult_0_right)
[PROOF STATE]
proof (state)
this:
b * c = 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
 2. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b * c = 0
[PROOF STEP]
have "(a::nat) mod (b*c) = a"
[PROOF STATE]
proof (prove)
using this:
b * c = 0

goal (1 subgoal):
 1. a mod (b * c) = a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a mod (b * c) = a

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
 2. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod (b * c) = a
[PROOF STEP]
have "((a::nat) mod (b*c)) mod c = a mod c"
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) = a

goal (1 subgoal):
 1. a mod (b * c) mod c = a mod c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a mod (b * c) mod c = a mod c

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
 2. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod (b * c) mod c = a mod c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) mod c = a mod c

goal (1 subgoal):
 1. a mod (b * c) mod c = a mod c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a mod (b * c) mod c = a mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
let ?x = "(a::nat) mod (b*c)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
let ?z = "?x mod c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
have "\<exists>m. a = m*(b*c) + ?x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. a = m * (b * c) + a mod (b * c)
[PROOF STEP]
by (metis div_mult_mod_eq)
[PROOF STATE]
proof (state)
this:
\<exists>m. a = m * (b * c) + a mod (b * c)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m. a = m * (b * c) + a mod (b * c)
[PROOF STEP]
obtain m1 where "a = m1*(b*c) + ?x"
[PROOF STATE]
proof (prove)
using this:
\<exists>m. a = m * (b * c) + a mod (b * c)

goal (1 subgoal):
 1. (\<And>m1. a = m1 * (b * c) + a mod (b * c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = m1 * (b * c) + a mod (b * c)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = m1 * (b * c) + a mod (b * c)
[PROOF STEP]
have "?x = (a - m1*(b*c))"
[PROOF STATE]
proof (prove)
using this:
a = m1 * (b * c) + a mod (b * c)

goal (1 subgoal):
 1. a mod (b * c) = a - m1 * (b * c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a mod (b * c) = a - m1 * (b * c)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod (b * c) = a - m1 * (b * c)
[PROOF STEP]
have "\<exists>m.( ?x = m*c + ?z)"
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) = a - m1 * (b * c)

goal (1 subgoal):
 1. \<exists>m. a mod (b * c) = m * c + a mod (b * c) mod c
[PROOF STEP]
using mod_div_decomp
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) = a - m1 * (b * c)
(\<And>q r. \<lbrakk>q = ?a div ?b; r = ?a mod ?b; ?a = q * ?b + r\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>m. a mod (b * c) = m * c + a mod (b * c) mod c
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m. a mod (b * c) = m * c + a mod (b * c) mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m. a mod (b * c) = m * c + a mod (b * c) mod c
[PROOF STEP]
obtain m where "( ?x = m*c + ?z)"
[PROOF STATE]
proof (prove)
using this:
\<exists>m. a mod (b * c) = m * c + a mod (b * c) mod c

goal (1 subgoal):
 1. (\<And>m. a mod (b * c) = m * c + a mod (b * c) mod c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a mod (b * c) = m * c + a mod (b * c) mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod (b * c) = m * c + a mod (b * c) mod c
[PROOF STEP]
have "(a - m1*(b*c)) = m*c + ?z"
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) = m * c + a mod (b * c) mod c

goal (1 subgoal):
 1. a - m1 * (b * c) = m * c + a mod (b * c) mod c
[PROOF STEP]
using  \<open>a mod (b * c) = a - m1 * (b * c)\<close>
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) = m * c + a mod (b * c) mod c
a mod (b * c) = a - m1 * (b * c)

goal (1 subgoal):
 1. a - m1 * (b * c) = m * c + a mod (b * c) mod c
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
a - m1 * (b * c) = m * c + a mod (b * c) mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a - m1 * (b * c) = m * c + a mod (b * c) mod c
[PROOF STEP]
have "a = m1*b*c + m*c + ?z"
[PROOF STATE]
proof (prove)
using this:
a - m1 * (b * c) = m * c + a mod (b * c) mod c

goal (1 subgoal):
 1. a = m1 * b * c + m * c + a mod (b * c) mod c
[PROOF STEP]
using \<open>a = m1 * (b * c) + a mod (b * c)\<close> \<open>a mod (b * c)
        = m * c + a mod (b * c) mod c\<close>
[PROOF STATE]
proof (prove)
using this:
a - m1 * (b * c) = m * c + a mod (b * c) mod c
a = m1 * (b * c) + a mod (b * c)
a mod (b * c) = m * c + a mod (b * c) mod c

goal (1 subgoal):
 1. a = m1 * b * c + m * c + a mod (b * c) mod c
[PROOF STEP]
by (metis  ab_semigroup_add_class.add_ac(1)
        ab_semigroup_mult_class.mult_ac(1))
[PROOF STATE]
proof (state)
this:
a = m1 * b * c + m * c + a mod (b * c) mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = m1 * b * c + m * c + a mod (b * c) mod c
[PROOF STEP]
have 1:"a = (m1*b + m)*c + ?z"
[PROOF STATE]
proof (prove)
using this:
a = m1 * b * c + m * c + a mod (b * c) mod c

goal (1 subgoal):
 1. a = (m1 * b + m) * c + a mod (b * c) mod c
[PROOF STEP]
by (metis add_mult_distrib2 mult.commute)
[PROOF STATE]
proof (state)
this:
a = (m1 * b + m) * c + a mod (b * c) mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
let ?y = "(a mod c)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
have "\<exists>n. a = n*(c) + ?y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. a = n * c + a mod c
[PROOF STEP]
by (metis "1" \<open>a mod (b * c) = m * c + a mod (b * c) mod c\<close> mod_mult_self3)
[PROOF STATE]
proof (state)
this:
\<exists>n. a = n * c + a mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. a = n * c + a mod c
[PROOF STEP]
obtain n where "a = n*(c) + ?y"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. a = n * c + a mod c

goal (1 subgoal):
 1. (\<And>n. a = n * c + a mod c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = n * c + a mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
a = (m1 * b + m) * c + a mod (b * c) mod c
a = n * c + a mod c
[PROOF STEP]
have "(m1*b + m)*c + ?z = n*c + ?y"
[PROOF STATE]
proof (prove)
using this:
a = (m1 * b + m) * c + a mod (b * c) mod c
a = n * c + a mod c

goal (1 subgoal):
 1. (m1 * b + m) * c + a mod (b * c) mod c = n * c + a mod c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(m1 * b + m) * c + a mod (b * c) mod c = n * c + a mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(m1 * b + m) * c + a mod (b * c) mod c = n * c + a mod c
[PROOF STEP]
have "(m1*b + m)*c - (n*c) = ?y - ?z"
[PROOF STATE]
proof (prove)
using this:
(m1 * b + m) * c + a mod (b * c) mod c = n * c + a mod c

goal (1 subgoal):
 1. (m1 * b + m) * c - n * c = a mod c - a mod (b * c) mod c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(m1 * b + m) * c - n * c = a mod c - a mod (b * c) mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(m1 * b + m) * c - n * c = a mod c - a mod (b * c) mod c
[PROOF STEP]
have "(m1*b + m - n)*c = (?y - ?z)"
[PROOF STATE]
proof (prove)
using this:
(m1 * b + m) * c - n * c = a mod c - a mod (b * c) mod c

goal (1 subgoal):
 1. (m1 * b + m - n) * c = a mod c - a mod (b * c) mod c
[PROOF STEP]
by (metis diff_mult_distrib2 mult.commute)
[PROOF STATE]
proof (state)
this:
(m1 * b + m - n) * c = a mod c - a mod (b * c) mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(m1 * b + m - n) * c = a mod c - a mod (b * c) mod c
[PROOF STEP]
have "c dvd (?y - ?z)"
[PROOF STATE]
proof (prove)
using this:
(m1 * b + m - n) * c = a mod c - a mod (b * c) mod c

goal (1 subgoal):
 1. c dvd a mod c - a mod (b * c) mod c
[PROOF STEP]
by (metis dvd_triv_right)
[PROOF STATE]
proof (state)
this:
c dvd a mod c - a mod (b * c) mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c dvd a mod c - a mod (b * c) mod c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
have "?y < c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod c < c
[PROOF STEP]
using mod_less_divisor False
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> ?m mod ?n < ?n
c \<noteq> 0

goal (1 subgoal):
 1. a mod c < c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a mod c < c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a mod c < c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
have "?z < c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod (b * c) mod c < c
[PROOF STEP]
using mod_less_divisor False
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> ?m mod ?n < ?n
c \<noteq> 0

goal (1 subgoal):
 1. a mod (b * c) mod c < c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a mod (b * c) mod c < c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a mod (b * c) mod c < c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
have "?y - ?z < c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod c - a mod (b * c) mod c < c
[PROOF STEP]
using calculation(2) less_imp_diff_less
[PROOF STATE]
proof (prove)
using this:
a mod c < c
?j < ?k \<Longrightarrow> ?j - ?n < ?k

goal (1 subgoal):
 1. a mod c - a mod (b * c) mod c < c
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a mod c - a mod (b * c) mod c < c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c dvd a mod c - a mod (b * c) mod c
a mod c < c
a mod (b * c) mod c < c
a mod c - a mod (b * c) mod c < c
[PROOF STEP]
have "?y - ?z = 0"
[PROOF STATE]
proof (prove)
using this:
c dvd a mod c - a mod (b * c) mod c
a mod c < c
a mod (b * c) mod c < c
a mod c - a mod (b * c) mod c < c

goal (1 subgoal):
 1. a mod c - a mod (b * c) mod c = 0
[PROOF STEP]
by (metis dvd_imp_mod_0 mod_less)
[PROOF STATE]
proof (state)
this:
a mod c - a mod (b * c) mod c = 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> a mod (b * c) mod c = a mod c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod c - a mod (b * c) mod c = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a mod c - a mod (b * c) mod c = 0

goal (1 subgoal):
 1. a mod (b * c) mod c = a mod c
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
a mod c - a mod (b * c) mod c = 0
c \<noteq> 0

goal (1 subgoal):
 1. a mod (b * c) mod c = a mod c
[PROOF STEP]
by (metis "1" mod_add_right_eq mod_mult_self2 add.commute mult.commute)
[PROOF STATE]
proof (state)
this:
a mod (b * c) mod c = a mod c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mod_div_relation:"((a::nat) mod (b*c)) div c = (a div c) mod b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod (b * c) div c = a div c mod b
[PROOF STEP]
proof(cases "b*c = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b * c = 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
 2. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b * c = 0

goal (2 subgoals):
 1. b * c = 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
 2. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
have T_1:"(b = 0)\<or>(c = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = 0 \<or> c = 0
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
b * c = 0

goal (1 subgoal):
 1. b = 0 \<or> c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b = 0 \<or> c = 0

goal (2 subgoals):
 1. b * c = 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
 2. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod (b * c) div c = a div c mod b
[PROOF STEP]
proof(cases "(b = 0)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
 2. b \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = 0

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
 2. b \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
have "a mod (b*c) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod (b * c) = a
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
b = 0

goal (1 subgoal):
 1. a mod (b * c) = a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a mod (b * c) = a

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
 2. b \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod (b * c) = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) = a

goal (1 subgoal):
 1. a mod (b * c) div c = a div c mod b
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) = a
b = 0

goal (1 subgoal):
 1. a mod (b * c) div c = a div c mod b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a mod (b * c) div c = a div c mod b

goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> 0

goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
have "c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = 0
[PROOF STEP]
using T_1 False
[PROOF STATE]
proof (prove)
using this:
b = 0 \<or> c = 0
b \<noteq> 0

goal (1 subgoal):
 1. c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c = 0

goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. a mod (b * c) div c = a div c mod b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a mod (b * c) div c = a div c mod b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a mod (b * c) div c = a div c mod b

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b * c \<noteq> 0

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
have F_1:"(b > 0)\<and> (c > 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < b \<and> 0 < c
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
b * c \<noteq> 0

goal (1 subgoal):
 1. 0 < b \<and> 0 < c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < b \<and> 0 < c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
have "\<exists>x. a = x*(b*c) + (a mod (b*c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. a = x * (b * c) + a mod (b * c)
[PROOF STEP]
using mod_div_decomp
[PROOF STATE]
proof (prove)
using this:
(\<And>q r. \<lbrakk>q = ?a div ?b; r = ?a mod ?b; ?a = q * ?b + r\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>x. a = x * (b * c) + a mod (b * c)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. a = x * (b * c) + a mod (b * c)

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. a = x * (b * c) + a mod (b * c)
[PROOF STEP]
obtain x where "a = x*(b*c) + (a mod (b*c))"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. a = x * (b * c) + a mod (b * c)

goal (1 subgoal):
 1. (\<And>x. a = x * (b * c) + a mod (b * c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = x * (b * c) + a mod (b * c)

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = x * (b * c) + a mod (b * c)
[PROOF STEP]
have "a div c = ((x*(b*c)) div c) + ((a mod (b*c)) div c)"
[PROOF STATE]
proof (prove)
using this:
a = x * (b * c) + a mod (b * c)

goal (1 subgoal):
 1. a div c = x * (b * c) div c + a mod (b * c) div c
[PROOF STEP]
using  div_add1_eq mod_add_self1 mod_add_self2
       mod_by_0 mod_div_trivial mod_prop1 mod_self
[PROOF STATE]
proof (prove)
using this:
a = x * (b * c) + a mod (b * c)
(?a + ?b) div ?c = ?a div ?c + ?b div ?c + (?a mod ?c + ?b mod ?c) div ?c
(?b + ?a) mod ?b = ?a mod ?b
(?a + ?b) mod ?b = ?a mod ?b
?a mod (0::?'a) = ?a
?a mod ?b div ?b = (0::?'a)
?a mod (?b * ?c) mod ?c = ?a mod ?c
?a mod ?a = (0::?'a)

goal (1 subgoal):
 1. a div c = x * (b * c) div c + a mod (b * c) div c
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
a div c = x * (b * c) div c + a mod (b * c) div c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a div c = x * (b * c) div c + a mod (b * c) div c
[PROOF STEP]
have "a div c = (((x*b)*c) div c) + ((a mod (b*c)) div c)"
[PROOF STATE]
proof (prove)
using this:
a div c = x * (b * c) div c + a mod (b * c) div c

goal (1 subgoal):
 1. a div c = x * b * c div c + a mod (b * c) div c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a div c = x * b * c div c + a mod (b * c) div c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a div c = x * b * c div c + a mod (b * c) div c
[PROOF STEP]
have F_2:"a div c = (x*b) + ((a mod (b*c)) div c)"
[PROOF STATE]
proof (prove)
using this:
a div c = x * b * c div c + a mod (b * c) div c

goal (1 subgoal):
 1. a div c = x * b + a mod (b * c) div c
[PROOF STEP]
by (metis F_1 nonzero_mult_div_cancel_left mult.commute neq0_conv)
[PROOF STATE]
proof (state)
this:
a div c = x * b + a mod (b * c) div c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
have "\<exists>y. a div c = (y*b) + ((a div c) mod b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. a div c = y * b + a div c mod b
[PROOF STEP]
by (metis add.commute mod_div_mult_eq)
[PROOF STATE]
proof (state)
this:
\<exists>y. a div c = y * b + a div c mod b

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. a div c = y * b + a div c mod b
[PROOF STEP]
obtain y where "a div c = (y*b) + ((a div c) mod b)"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. a div c = y * b + a div c mod b

goal (1 subgoal):
 1. (\<And>y. a div c = y * b + a div c mod b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a div c = y * b + a div c mod b

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
with F_2
[PROOF STATE]
proof (chain)
picking this:
a div c = x * b + a mod (b * c) div c
a div c = y * b + a div c mod b
[PROOF STEP]
have F_3:" (x*b) + ((a mod (b*c)) div c) = (y*b) + ((a div c) mod b)"
[PROOF STATE]
proof (prove)
using this:
a div c = x * b + a mod (b * c) div c
a div c = y * b + a div c mod b

goal (1 subgoal):
 1. x * b + a mod (b * c) div c = y * b + a div c mod b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x * b + a mod (b * c) div c = y * b + a div c mod b

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x * b + a mod (b * c) div c = y * b + a div c mod b
[PROOF STEP]
have "(x*b) - (y * b) = ((a div c) mod b) - ((a mod (b*c)) div c) "
[PROOF STATE]
proof (prove)
using this:
x * b + a mod (b * c) div c = y * b + a div c mod b

goal (1 subgoal):
 1. x * b - y * b = a div c mod b - a mod (b * c) div c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x * b - y * b = a div c mod b - a mod (b * c) div c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x * b - y * b = a div c mod b - a mod (b * c) div c
[PROOF STEP]
have "(x - y) * b = ((a div c) mod b) - ((a mod (b*c)) div c)"
[PROOF STATE]
proof (prove)
using this:
x * b - y * b = a div c mod b - a mod (b * c) div c

goal (1 subgoal):
 1. (x - y) * b = a div c mod b - a mod (b * c) div c
[PROOF STEP]
by (metis diff_mult_distrib2 mult.commute)
[PROOF STATE]
proof (state)
this:
(x - y) * b = a div c mod b - a mod (b * c) div c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x - y) * b = a div c mod b - a mod (b * c) div c
[PROOF STEP]
have F_4:"b dvd (((a div c) mod b) - ((a mod (b*c)) div c))"
[PROOF STATE]
proof (prove)
using this:
(x - y) * b = a div c mod b - a mod (b * c) div c

goal (1 subgoal):
 1. b dvd a div c mod b - a mod (b * c) div c
[PROOF STEP]
by (metis dvd_eq_mod_eq_0 mod_mult_self1_is_0 mult.commute)
[PROOF STATE]
proof (state)
this:
b dvd a div c mod b - a mod (b * c) div c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
have F_5:"b >  ((a div c) mod b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div c mod b < b
[PROOF STEP]
by (metis F_1 mod_less_divisor)
[PROOF STATE]
proof (state)
this:
a div c mod b < b

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
have "b*c > (a mod (b*c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod (b * c) < b * c
[PROOF STEP]
by (metis False mod_less_divisor neq0_conv)
[PROOF STATE]
proof (state)
this:
a mod (b * c) < b * c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a mod (b * c) < b * c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod (b * c) < b * c
[PROOF STEP]
have "(b*c) div c > (a mod (b*c)) div c"
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) < b * c

goal (1 subgoal):
 1. a mod (b * c) div c < b * c div c
[PROOF STEP]
by (metis F_1 div_left_ineq nonzero_mult_div_cancel_right neq0_conv)
[PROOF STATE]
proof (state)
this:
a mod (b * c) div c < b * c div c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod (b * c) div c < b * c div c
[PROOF STEP]
have "b > (a mod (b*c)) div c"
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) div c < b * c div c

goal (1 subgoal):
 1. a mod (b * c) div c < b
[PROOF STEP]
by (metis calculation div_right_ineq mult.commute)
[PROOF STATE]
proof (state)
this:
a mod (b * c) div c < b

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
with F_4 F_5
[PROOF STATE]
proof (chain)
picking this:
b dvd a div c mod b - a mod (b * c) div c
a div c mod b < b
a mod (b * c) div c < b
[PROOF STEP]
have F_6:"((a div c) mod b)-((a mod (b*c)) div c) = 0"
[PROOF STATE]
proof (prove)
using this:
b dvd a div c mod b - a mod (b * c) div c
a div c mod b < b
a mod (b * c) div c < b

goal (1 subgoal):
 1. a div c mod b - a mod (b * c) div c = 0
[PROOF STEP]
using less_imp_diff_less nat_dvd_not_less
[PROOF STATE]
proof (prove)
using this:
b dvd a div c mod b - a mod (b * c) div c
a div c mod b < b
a mod (b * c) div c < b
?j < ?k \<Longrightarrow> ?j - ?n < ?k
\<lbrakk>0 < ?m; ?m < ?n\<rbrakk> \<Longrightarrow> \<not> ?n dvd ?m

goal (1 subgoal):
 1. a div c mod b - a mod (b * c) div c = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a div c mod b - a mod (b * c) div c = 0

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
from F_3
[PROOF STATE]
proof (chain)
picking this:
x * b + a mod (b * c) div c = y * b + a div c mod b
[PROOF STEP]
have "(y * b) - (x*b)
                      = ((a mod (b*c)) div c) - ((a div c) mod b) "
[PROOF STATE]
proof (prove)
using this:
x * b + a mod (b * c) div c = y * b + a div c mod b

goal (1 subgoal):
 1. y * b - x * b = a mod (b * c) div c - a div c mod b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y * b - x * b = a mod (b * c) div c - a div c mod b

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y * b - x * b = a mod (b * c) div c - a div c mod b
[PROOF STEP]
have "(y - x) * b = ((a mod (b*c)) div c) - ((a div c) mod b)"
[PROOF STATE]
proof (prove)
using this:
y * b - x * b = a mod (b * c) div c - a div c mod b

goal (1 subgoal):
 1. (y - x) * b = a mod (b * c) div c - a div c mod b
[PROOF STEP]
by (metis diff_mult_distrib2 mult.commute)
[PROOF STATE]
proof (state)
this:
(y - x) * b = a mod (b * c) div c - a div c mod b

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(y - x) * b = a mod (b * c) div c - a div c mod b
[PROOF STEP]
have F_7:"b dvd (((a mod (b*c)) div c) - ((a div c) mod b))"
[PROOF STATE]
proof (prove)
using this:
(y - x) * b = a mod (b * c) div c - a div c mod b

goal (1 subgoal):
 1. b dvd a mod (b * c) div c - a div c mod b
[PROOF STEP]
by (metis dvd_eq_mod_eq_0 mod_mult_self1_is_0  mult.commute)
[PROOF STATE]
proof (state)
this:
b dvd a mod (b * c) div c - a div c mod b

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
have F_8:"b >  ((a div c) mod b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div c mod b < b
[PROOF STEP]
by (metis F_1 mod_less_divisor)
[PROOF STATE]
proof (state)
this:
a div c mod b < b

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
have "b*c > (a mod (b*c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod (b * c) < b * c
[PROOF STEP]
by (metis False mod_less_divisor neq0_conv)
[PROOF STATE]
proof (state)
this:
a mod (b * c) < b * c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a mod (b * c) < b * c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod (b * c) < b * c
[PROOF STEP]
have "(b*c) div c > (a mod (b*c)) div c"
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) < b * c

goal (1 subgoal):
 1. a mod (b * c) div c < b * c div c
[PROOF STEP]
by (metis F_1 div_left_ineq  nonzero_mult_div_cancel_right neq0_conv)
[PROOF STATE]
proof (state)
this:
a mod (b * c) div c < b * c div c

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod (b * c) div c < b * c div c
[PROOF STEP]
have "b > (a mod (b*c)) div c"
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) div c < b * c div c

goal (1 subgoal):
 1. a mod (b * c) div c < b
[PROOF STEP]
by (metis calculation div_right_ineq  mult.commute)
[PROOF STATE]
proof (state)
this:
a mod (b * c) div c < b

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
with F_7 F_8
[PROOF STATE]
proof (chain)
picking this:
b dvd a mod (b * c) div c - a div c mod b
a div c mod b < b
a mod (b * c) div c < b
[PROOF STEP]
have "((a mod (b*c)) div c) - ((a div c) mod b) = 0"
[PROOF STATE]
proof (prove)
using this:
b dvd a mod (b * c) div c - a div c mod b
a div c mod b < b
a mod (b * c) div c < b

goal (1 subgoal):
 1. a mod (b * c) div c - a div c mod b = 0
[PROOF STEP]
by (metis F_2 cancel_comm_monoid_add_class.diff_cancel mod_if mod_mult_self3)
[PROOF STATE]
proof (state)
this:
a mod (b * c) div c - a div c mod b = 0

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
with F_6
[PROOF STATE]
proof (chain)
picking this:
a div c mod b - a mod (b * c) div c = 0
a mod (b * c) div c - a div c mod b = 0
[PROOF STEP]
have "((a mod (b*c)) div c) = ((a div c) mod b)"
[PROOF STATE]
proof (prove)
using this:
a div c mod b - a mod (b * c) div c = 0
a mod (b * c) div c - a div c mod b = 0

goal (1 subgoal):
 1. a mod (b * c) div c = a div c mod b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a mod (b * c) div c = a div c mod b

goal (1 subgoal):
 1. b * c \<noteq> 0 \<Longrightarrow> a mod (b * c) div c = a div c mod b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod (b * c) div c = a div c mod b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) div c = a div c mod b

goal (1 subgoal):
 1. a mod (b * c) div c = a div c mod b
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
a mod (b * c) div c = a div c mod b
b * c \<noteq> 0

goal (1 subgoal):
 1. a mod (b * c) div c = a div c mod b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a mod (b * c) div c = a div c mod b

goal:
No subgoals!
[PROOF STEP]
qed