[STATEMENT]
lemma floor_div_pos_int: 
  fixes r :: "'a :: floor_ceiling"
  assumes n: "n > 0" 
  shows "\<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
let ?of_int = "of_int :: int \<Rightarrow> 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
define rhs where "rhs = \<lfloor>r\<rfloor> div n"
[PROOF STATE]
proof (state)
this:
rhs = \<lfloor>r\<rfloor> div n

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
let ?n = "?of_int n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
define m where "m = \<lfloor>r\<rfloor> mod n"
[PROOF STATE]
proof (state)
this:
m = \<lfloor>r\<rfloor> mod n

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
let ?m = "?of_int m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
from div_mult_mod_eq[of "floor r" n]
[PROOF STATE]
proof (chain)
picking this:
\<lfloor>r\<rfloor> div n * n + \<lfloor>r\<rfloor> mod n = \<lfloor>r\<rfloor>
[PROOF STEP]
have dm: "rhs * n + m = \<lfloor>r\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<lfloor>r\<rfloor> div n * n + \<lfloor>r\<rfloor> mod n = \<lfloor>r\<rfloor>

goal (1 subgoal):
 1. rhs * n + m = \<lfloor>r\<rfloor>
[PROOF STEP]
unfolding rhs_def m_def
[PROOF STATE]
proof (prove)
using this:
\<lfloor>r\<rfloor> div n * n + \<lfloor>r\<rfloor> mod n = \<lfloor>r\<rfloor>

goal (1 subgoal):
 1. \<lfloor>r\<rfloor> div n * n + \<lfloor>r\<rfloor> mod n = \<lfloor>r\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rhs * n + m = \<lfloor>r\<rfloor>

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have mn: "m < n" and m0: "m \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < n &&& 0 \<le> m
[PROOF STEP]
using n m_def
[PROOF STATE]
proof (prove)
using this:
0 < n
m = \<lfloor>r\<rfloor> mod n

goal (1 subgoal):
 1. m < n &&& 0 \<le> m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m < n
0 \<le> m

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
define e where "e = r - ?of_int \<lfloor>r\<rfloor>"
[PROOF STATE]
proof (state)
this:
e = r - of_int \<lfloor>r\<rfloor>

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have e0: "e \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> e
[PROOF STEP]
unfolding e_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> r - of_int \<lfloor>r\<rfloor>
[PROOF STEP]
by (metis diff_self eq_iff floor_diff_of_int zero_le_floor)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> e

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have e1: "e < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e < (1::'a)
[PROOF STEP]
unfolding e_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r - of_int \<lfloor>r\<rfloor> < (1::'a)
[PROOF STEP]
by (metis diff_self dual_order.refl floor_diff_of_int floor_le_zero)
[PROOF STATE]
proof (state)
this:
e < (1::'a)

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have "r = ?of_int \<lfloor>r\<rfloor> + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = of_int \<lfloor>r\<rfloor> + e
[PROOF STEP]
unfolding e_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = of_int \<lfloor>r\<rfloor> + (r - of_int \<lfloor>r\<rfloor>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r = of_int \<lfloor>r\<rfloor> + e

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r = of_int \<lfloor>r\<rfloor> + e

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have "\<lfloor>r\<rfloor> = rhs * n + m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>r\<rfloor> = rhs * n + m
[PROOF STEP]
using dm
[PROOF STATE]
proof (prove)
using this:
rhs * n + m = \<lfloor>r\<rfloor>

goal (1 subgoal):
 1. \<lfloor>r\<rfloor> = rhs * n + m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lfloor>r\<rfloor> = rhs * n + m

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
r = of_int (rhs * n + m) + e
[PROOF STEP]
have "r = ?of_int (rhs * n + m) + e"
[PROOF STATE]
proof (prove)
using this:
r = of_int (rhs * n + m) + e

goal (1 subgoal):
 1. r = of_int (rhs * n + m) + e
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
r = of_int (rhs * n + m) + e

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
hence "r / ?n = ?of_int (rhs * n) / ?n + (e + ?m) / ?n"
[PROOF STATE]
proof (prove)
using this:
r = of_int (rhs * n + m) + e

goal (1 subgoal):
 1. r / of_int n = of_int (rhs * n) / of_int n + (e + of_int m) / of_int n
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
r = of_int (rhs * n + m) + e
0 < n

goal (1 subgoal):
 1. r / of_int n = of_int (rhs * n) / of_int n + (e + of_int m) / of_int n
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
r / of_int n = of_int (rhs * n) / of_int n + (e + of_int m) / of_int n

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r / of_int n = of_int (rhs * n) / of_int n + (e + of_int m) / of_int n

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have "?of_int (rhs * n) / ?n = ?of_int rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (rhs * n) / of_int n = of_int rhs
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. of_int (rhs * n) / of_int n = of_int rhs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int (rhs * n) / of_int n = of_int rhs

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
r / of_int n = of_int rhs + (e + of_int m) / of_int n
[PROOF STEP]
have *: "r / ?of_int n = (e + ?of_int m) / ?of_int n + ?of_int rhs"
[PROOF STATE]
proof (prove)
using this:
r / of_int n = of_int rhs + (e + of_int m) / of_int n

goal (1 subgoal):
 1. r / of_int n = (e + of_int m) / of_int n + of_int rhs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r / of_int n = (e + of_int m) / of_int n + of_int rhs

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have "?l = rhs + floor ((e + ?m) / ?n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = rhs + \<lfloor>(e + of_int m) / of_int n\<rfloor>
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(e + of_int m) / of_int n + of_int rhs\<rfloor> = rhs + \<lfloor>(e + of_int m) / of_int n\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lfloor>r / of_int n\<rfloor> = rhs + \<lfloor>(e + of_int m) / of_int n\<rfloor>

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>r / of_int n\<rfloor> = rhs + \<lfloor>(e + of_int m) / of_int n\<rfloor>

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
have "floor ((e + ?m) / ?n) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(e + of_int m) / of_int n\<rfloor> = 0
[PROOF STEP]
proof (rule floor_unique)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. of_int 0 \<le> (e + of_int m) / of_int n
 2. (e + of_int m) / of_int n < of_int 0 + (1::'a)
[PROOF STEP]
show "?of_int 0 \<le> (e + ?m) / ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int 0 \<le> (e + of_int m) / of_int n
[PROOF STEP]
using e0 m0 n
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> e
0 \<le> m
0 < n

goal (1 subgoal):
 1. of_int 0 \<le> (e + of_int m) / of_int n
[PROOF STEP]
by (metis add_increasing2 divide_nonneg_pos of_int_0 of_int_0_le_iff of_int_0_less_iff)
[PROOF STATE]
proof (state)
this:
of_int 0 \<le> (e + of_int m) / of_int n

goal (1 subgoal):
 1. (e + of_int m) / of_int n < of_int 0 + (1::'a)
[PROOF STEP]
show "(e + ?m) / ?n < ?of_int 0 + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (e + of_int m) / of_int n < of_int 0 + (1::'a)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have n': "?n > 0" "?n \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (0::'a) < of_int n &&& (0::'a) \<le> of_int n
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
(0::'a) < of_int n
(0::'a) \<le> of_int n

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> (e + of_int m) / of_int n < of_int 0 + (1::'a)

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
hence "(e + ?m) / ?n \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
\<not> (e + of_int m) / of_int n < of_int 0 + (1::'a)

goal (1 subgoal):
 1. (1::'a) \<le> (e + of_int m) / of_int n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1::'a) \<le> (e + of_int m) / of_int n

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
from mult_right_mono[OF this n'(2)]
[PROOF STATE]
proof (chain)
picking this:
(1::'a) * of_int n \<le> (e + of_int m) / of_int n * of_int n
[PROOF STEP]
have "?n \<le> e + ?m"
[PROOF STATE]
proof (prove)
using this:
(1::'a) * of_int n \<le> (e + of_int m) / of_int n * of_int n

goal (1 subgoal):
 1. of_int n \<le> e + of_int m
[PROOF STEP]
using n'(1)
[PROOF STATE]
proof (prove)
using this:
(1::'a) * of_int n \<le> (e + of_int m) / of_int n * of_int n
(0::'a) < of_int n

goal (1 subgoal):
 1. of_int n \<le> e + of_int m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_int n \<le> e + of_int m

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int n \<le> e + of_int m

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
have "?m \<le> ?n - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int m \<le> of_int n - (1::'a)
[PROOF STEP]
using mn
[PROOF STATE]
proof (prove)
using this:
m < n

goal (1 subgoal):
 1. of_int m \<le> of_int n - (1::'a)
[PROOF STEP]
by (metis of_int_1 of_int_diff of_int_le_iff zle_diff1_eq)
[PROOF STATE]
proof (state)
this:
of_int m \<le> of_int n - (1::'a)

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> e + x \<le> e + y) \<Longrightarrow> of_int n \<le> e + (of_int n - (1::'a))
[PROOF STEP]
have "?n \<le> e + ?n - 1"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> e + x \<le> e + y) \<Longrightarrow> of_int n \<le> e + (of_int n - (1::'a))

goal (1 subgoal):
 1. of_int n \<le> e + of_int n - (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int n \<le> e + of_int n - (1::'a)

goal (1 subgoal):
 1. \<not> (e + of_int m) / of_int n < of_int 0 + (1::'a) \<Longrightarrow> False
[PROOF STEP]
with e1
[PROOF STATE]
proof (chain)
picking this:
e < (1::'a)
of_int n \<le> e + of_int n - (1::'a)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
e < (1::'a)
of_int n \<le> e + of_int n - (1::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(e + of_int m) / of_int n < of_int 0 + (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lfloor>(e + of_int m) / of_int n\<rfloor> = 0

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lfloor>r / of_int n\<rfloor> = rhs + 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lfloor>r / of_int n\<rfloor> = rhs + 0

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
unfolding rhs_def
[PROOF STATE]
proof (prove)
using this:
\<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n + 0

goal (1 subgoal):
 1. \<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lfloor>r / of_int n\<rfloor> = \<lfloor>r\<rfloor> div n

goal:
No subgoals!
[PROOF STEP]
qed