[STATEMENT]
lemma pre_hensel:
"val_Zp (a \<ominus> (ns n)) >  val_Zp (f'\<bullet>a)"
"\<exists>N. \<forall>n. n> N \<longrightarrow> (val_Zp (a \<ominus> (ns n)) = val_Zp (divide (f\<bullet>a) (f'\<bullet>a)))"
"val_Zp (f'\<bullet>(ns n)) = val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns n) &&& \<exists>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) &&& val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns n)
 2. \<exists>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
 3. val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
[PROOF STEP]
show "val_Zp (a \<ominus> (ns n)) >  val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns n)
[PROOF STEP]
proof(induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns 0)
 2. \<And>n. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns n) \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns 0)
 2. \<And>n. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns n) \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns 0)
[PROOF STEP]
by (simp add: val_Zp_def)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns 0)

goal (1 subgoal):
 1. \<And>n. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns n) \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns n) \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns n)

goal (1 subgoal):
 1. \<And>n. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns n) \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
show "val_Zp (a \<ominus> (ns (Suc n))) > val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
have I0: "val_Zp ((ns (Suc n)) \<ominus> (ns n)) >  val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
proof(cases "(ns (Suc n)) = (ns n)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ns (Suc n) = ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
 2. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ns (Suc n) = ns n

goal (2 subgoals):
 1. ns (Suc n) = ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
 2. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ns (Suc n) = ns n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns (Suc n) = ns n

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
by (simp add: newton_seq_closed val_Zp_def)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
ns (Suc n) \<noteq> ns n

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
have 00:"(ns (Suc n)) \<ominus> (ns n) = \<ominus>divide (f\<bullet>(ns n)) (f'\<bullet>(ns n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns (Suc n) \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
[PROOF STEP]
using  newton_seq_fact7
[PROOF STATE]
proof (prove)
using this:
ns (Suc ?n) \<ominus> ns ?n = \<ominus> local.divide (f \<bullet> ns ?n) (f' \<bullet> ns ?n)

goal (1 subgoal):
 1. ns (Suc n) \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns (Suc n) \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ns (Suc n) \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
[PROOF STEP]
have 0: "val_Zp((ns (Suc n)) \<ominus> (ns n)) = val_Zp (divide (f\<bullet>(ns n)) (f'\<bullet>(ns n)))"
[PROOF STATE]
proof (prove)
using this:
ns (Suc n) \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)

goal (1 subgoal):
 1. val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n))
[PROOF STEP]
using newton_seq_fact5 val_Zp_of_minus
[PROOF STATE]
proof (prove)
using this:
ns (Suc n) \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
local.divide (f \<bullet> ns ?l) (f' \<bullet> ns ?l) \<in> carrier Zp
?a \<in> carrier Zp \<Longrightarrow> val_Zp ?a = val_Zp (\<ominus> ?a)

goal (1 subgoal):
 1. val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n))

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
have 1: "(f\<bullet>(ns n)) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
by (metis False R.minus_zero R.r_right_minus_eq 00 divide_def f_closed to_fun_closed
              newton_seq_closed not_nonzero_Zp)
[PROOF STATE]
proof (state)
this:
f \<bullet> ns n \<in> nonzero Zp

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
have 2: "f'\<bullet>(ns n) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> ns n \<in> nonzero Zp
[PROOF STEP]
by (simp add: newton_seq_fact6)
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns n \<in> nonzero Zp

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
have "val_Zp (f\<bullet>(ns n))  \<ge> val_Zp (f'\<bullet>(ns n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
using nonzero_memE  \<open>f \<bullet> ns n \<in> nonzero Zp\<close> newton_seq_fact4
[PROOF STATE]
proof (prove)
using this:
?a \<in> nonzero Zp \<Longrightarrow> ?a \<in> carrier Zp
?a \<in> nonzero Zp \<Longrightarrow> ?a \<noteq> \<zero>
f \<bullet> ns n \<in> nonzero Zp
f \<bullet> ns ?l \<noteq> \<zero> \<Longrightarrow> val_Zp (f' \<bullet> ns ?l) \<le> val_Zp (f \<bullet> ns ?l)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
have 3:"val_Zp((ns (Suc n)) \<ominus> (ns n)) = val_Zp (f\<bullet>(ns n)) - val_Zp (f'\<bullet>(ns n))"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n)
[PROOF STEP]
using 0 1 2 newton_seq_fact9 nonzero_memE(2)
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns n) \<le> val_Zp (f \<bullet> ns n)
val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (local.divide (f \<bullet> ns n) (f' \<bullet> ns n))
f \<bullet> ns n \<in> nonzero Zp
f' \<bullet> ns n \<in> nonzero Zp
f \<bullet> ns ?n \<noteq> \<zero> \<Longrightarrow> val_Zp (ns (Suc ?n) \<ominus> ns ?n) = val_Zp (f \<bullet> ns ?n) - val_Zp (f' \<bullet> ns ?n)
?a \<in> nonzero Zp \<Longrightarrow> ?a \<noteq> \<zero>

goal (1 subgoal):
 1. val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n)

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
have 4: "val_Zp (f \<bullet> ns n) \<ge> (2 * val_Zp (f'\<bullet>a)) + 2 ^ n * t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
using newton_seq_fact2[of n]
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)
[PROOF STEP]
have 5: "val_Zp((ns (Suc n)) \<ominus> (ns n)) \<ge> ((2 * val_Zp (f'\<bullet>a)) + 2 ^ n * t) - val_Zp (f'\<bullet>(ns n))"
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> ns n) \<le> val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
using "3" eint_minus_ineq f'a_not_infinite newton_seq_fact1
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (f \<bullet> ns n)
val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (f \<bullet> ns n) - val_Zp (f' \<bullet> ns n)
\<lbrakk>?c \<noteq> \<infinity>; ?d \<le> ?b\<rbrakk> \<Longrightarrow> ?d - ?c \<le> ?b - ?c
val_Zp (f' \<bullet> a) \<noteq> \<infinity>
val_Zp (f' \<bullet> ns ?k) = val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> ns n) \<le> val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> ns n) \<le> val_Zp (ns (Suc n) \<ominus> ns n)

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
have 6: "((ns (Suc n)) \<ominus> (ns n)) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns (Suc n) \<ominus> ns n \<in> nonzero Zp
[PROOF STEP]
using False not_eq_diff_nonzero newton_seq_closed
[PROOF STATE]
proof (prove)
using this:
ns (Suc n) \<noteq> ns n
\<lbrakk>?a \<noteq> ?b; ?a \<in> carrier Zp; ?b \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?a \<ominus> ?b \<in> nonzero Zp
ns ?m \<in> carrier Zp

goal (1 subgoal):
 1. ns (Suc n) \<ominus> ns n \<in> nonzero Zp
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns (Suc n) \<ominus> ns n \<in> nonzero Zp

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ns (Suc n) \<ominus> ns n \<in> nonzero Zp
[PROOF STEP]
have "val_Zp((ns (Suc n)) \<ominus> (ns n)) \<ge> (2 * val_Zp (f'\<bullet>a)) + 2 ^ n * t - val_Zp ((f'\<bullet>a))"
[PROOF STATE]
proof (prove)
using this:
ns (Suc n) \<ominus> ns n \<in> nonzero Zp

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) \<le> val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
using "5"
[PROOF STATE]
proof (prove)
using this:
ns (Suc n) \<ominus> ns n \<in> nonzero Zp
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> ns n) \<le> val_Zp (ns (Suc n) \<ominus> ns n)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) \<le> val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) \<le> val_Zp (ns (Suc n) \<ominus> ns n)

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) \<le> val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
have 7: "val_Zp((ns (Suc n)) \<ominus> (ns n)) \<ge> (val_Zp (f'\<bullet>a)) + 2 ^ n * t"
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ n) * t - val_Zp (f' \<bullet> a) \<le> val_Zp (ns (Suc n) \<ominus> ns n)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
by (simp add: eint_minus_comm)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (ns (Suc n) \<ominus> ns n)

goal (1 subgoal):
 1. ns (Suc n) \<noteq> ns n \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
show  "val_Zp((ns (Suc n)) \<ominus> (ns n)) > (val_Zp (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (ns (Suc n) \<ominus> ns n)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
using f'a_not_infinite ge_plus_pos_imp_gt t_times_pow_pos
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) + eint (2 ^ n) * t \<le> val_Zp (ns (Suc n) \<ominus> ns n)
val_Zp (f' \<bullet> a) \<noteq> \<infinity>
\<lbrakk>?c \<noteq> \<infinity>; 0 < ?b; ?c + ?b \<le> ?d\<rbrakk> \<Longrightarrow> ?c < ?d
0 < eint (2 ^ ?n) * t

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
have "val_Zp ((ns (Suc n)) \<ominus> (ns n)) = val_Zp ((ns n) \<ominus> (ns (Suc n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (ns n \<ominus> ns (Suc n))
[PROOF STEP]
using  newton_seq_closed[of "n"]  newton_seq_closed[of "Suc n"]
                 val_Zp_def val_Zp_dist_def val_Zp_dist_sym val_Zp_def
[PROOF STATE]
proof (prove)
using this:
ns n \<in> carrier Zp
ns (Suc n) \<in> carrier Zp
val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))
val_Zp_dist ?a ?b \<equiv> val_Zp (?a \<ominus> ?b)
\<lbrakk>?a \<in> carrier Zp; ?b \<in> carrier Zp\<rbrakk> \<Longrightarrow> val_Zp_dist ?a ?b = val_Zp_dist ?b ?a
val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))

goal (1 subgoal):
 1. val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (ns n \<ominus> ns (Suc n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (ns n \<ominus> ns (Suc n))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (ns n \<ominus> ns (Suc n))
[PROOF STEP]
have I1: "val_Zp ((ns n) \<ominus> (ns (Suc n))) > val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
using this:
val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (ns n \<ominus> ns (Suc n))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (ns n \<ominus> ns (Suc n))
[PROOF STEP]
using I0
[PROOF STATE]
proof (prove)
using this:
val_Zp (ns (Suc n) \<ominus> ns n) = val_Zp (ns n \<ominus> ns (Suc n))
val_Zp (f' \<bullet> a) < val_Zp (ns (Suc n) \<ominus> ns n)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (ns n \<ominus> ns (Suc n))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (ns n \<ominus> ns (Suc n))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
have I2: " (a \<ominus> (ns n)) \<oplus> ((ns n) \<ominus> (ns (Suc n))) = (a \<ominus> (ns (Suc n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<ominus> ns n \<oplus> (ns n \<ominus> ns (Suc n)) = a \<ominus> ns (Suc n)
[PROOF STEP]
by (metis R.plus_diff_simp add_comm local.a_closed newton_seq_closed)
[PROOF STATE]
proof (state)
this:
a \<ominus> ns n \<oplus> (ns n \<ominus> ns (Suc n)) = a \<ominus> ns (Suc n)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<ominus> ns n \<oplus> (ns n \<ominus> ns (Suc n)) = a \<ominus> ns (Suc n)
[PROOF STEP]
have "val_Zp (a \<ominus> (ns (Suc n))) \<ge> min (val_Zp (a \<ominus> ns n)) (val_Zp (ns n \<ominus> ns (Suc n)))"
[PROOF STATE]
proof (prove)
using this:
a \<ominus> ns n \<oplus> (ns n \<ominus> ns (Suc n)) = a \<ominus> ns (Suc n)

goal (1 subgoal):
 1. min (val_Zp (a \<ominus> ns n)) (val_Zp (ns n \<ominus> ns (Suc n))) \<le> val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
by (metis R.minus_closed local.a_closed newton_seq_closed val_Zp_ultrametric)
[PROOF STATE]
proof (state)
this:
min (val_Zp (a \<ominus> ns n)) (val_Zp (ns n \<ominus> ns (Suc n))) \<le> val_Zp (a \<ominus> ns (Suc n))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
min (val_Zp (a \<ominus> ns n)) (val_Zp (ns n \<ominus> ns (Suc n))) \<le> val_Zp (a \<ominus> ns (Suc n))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
using I1 Suc.IH eint_min_ineq
[PROOF STATE]
proof (prove)
using this:
min (val_Zp (a \<ominus> ns n)) (val_Zp (ns n \<ominus> ns (Suc n))) \<le> val_Zp (a \<ominus> ns (Suc n))
val_Zp (f' \<bullet> a) < val_Zp (ns n \<ominus> ns (Suc n))
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns n)
\<lbrakk>min ?c ?d \<le> ?b; ?e < ?c; ?e < ?d\<rbrakk> \<Longrightarrow> ?e < ?b

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns n)

goal (2 subgoals):
 1. \<exists>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
 2. val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
[PROOF STEP]
show "val_Zp (f'\<bullet>(ns n)) = val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
[PROOF STEP]
using newton_seq_fact1
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns ?k) = val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns n) = val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. \<exists>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
show "\<exists>N.\<forall>n. n> N \<longrightarrow> (val_Zp (a \<ominus> (ns n)) = val_Zp (divide (f\<bullet>a) (f'\<bullet>a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have P: "\<And>m. m > 1 \<Longrightarrow> (val_Zp (a \<ominus> (ns m)) = val_Zp (divide (f\<bullet>a) (f'\<bullet>a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. 1 < m \<Longrightarrow> val_Zp (a \<ominus> ns m) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. 1 < m \<Longrightarrow> val_Zp (a \<ominus> ns m) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
fix n::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. 1 < m \<Longrightarrow> val_Zp (a \<ominus> ns m) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
assume AA: "n >1"
[PROOF STATE]
proof (state)
this:
1 < n

goal (1 subgoal):
 1. \<And>m. 1 < m \<Longrightarrow> val_Zp (a \<ominus> ns m) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
show " (val_Zp (a \<ominus> (ns n)) = val_Zp (divide (f\<bullet>a) (f'\<bullet>a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
proof(cases "(ns 1) = a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ns 1 = a \<Longrightarrow> val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
 2. ns 1 \<noteq> a \<Longrightarrow> val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ns 1 = a

goal (2 subgoals):
 1. ns 1 = a \<Longrightarrow> val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
 2. ns 1 \<noteq> a \<Longrightarrow> val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have T0: "\<And>k. \<forall>n. n \<le> k \<longrightarrow>  ns n = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<forall>n\<le>k. ns n = a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<forall>n\<le>k. ns n = a
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<forall>n\<le>k. ns n = a
[PROOF STEP]
show " \<forall>n. n \<le> k \<longrightarrow>  ns n = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<le>k. ns n = a
[PROOF STEP]
proof(induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>n\<le>0. ns n = a
 2. \<And>k. \<forall>n\<le>k. ns n = a \<Longrightarrow> \<forall>n\<le>Suc k. ns n = a
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<forall>n\<le>0. ns n = a
 2. \<And>k. \<forall>n\<le>k. ns n = a \<Longrightarrow> \<forall>n\<le>Suc k. ns n = a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<le>0. ns n = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>n\<le>0. ns n = a

goal (1 subgoal):
 1. \<And>k. \<forall>n\<le>k. ns n = a \<Longrightarrow> \<forall>n\<le>Suc k. ns n = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<forall>n\<le>k. ns n = a \<Longrightarrow> \<forall>n\<le>Suc k. ns n = a
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<forall>n\<le>k. ns n = a

goal (1 subgoal):
 1. \<And>k. \<forall>n\<le>k. ns n = a \<Longrightarrow> \<forall>n\<le>Suc k. ns n = a
[PROOF STEP]
show "\<forall>n\<le>Suc k. ns n = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<le>Suc k. ns n = a
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n \<le> Suc k \<Longrightarrow> ns n = a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<le> Suc k \<Longrightarrow> ns n = a
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<le> Suc k \<Longrightarrow> ns n = a
[PROOF STEP]
assume A: "n \<le>Suc k"
[PROOF STATE]
proof (state)
this:
n \<le> Suc k

goal (1 subgoal):
 1. \<And>n. n \<le> Suc k \<Longrightarrow> ns n = a
[PROOF STEP]
show "ns n = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns n = a
[PROOF STEP]
proof(cases "n < Suc k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n < Suc k \<Longrightarrow> ns n = a
 2. \<not> n < Suc k \<Longrightarrow> ns n = a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n < Suc k

goal (2 subgoals):
 1. n < Suc k \<Longrightarrow> ns n = a
 2. \<not> n < Suc k \<Longrightarrow> ns n = a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < Suc k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n < Suc k

goal (1 subgoal):
 1. ns n = a
[PROOF STEP]
using Suc.IH
[PROOF STATE]
proof (prove)
using this:
n < Suc k
\<forall>n\<le>k. ns n = a

goal (1 subgoal):
 1. ns n = a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ns n = a

goal (1 subgoal):
 1. \<not> n < Suc k \<Longrightarrow> ns n = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n < Suc k \<Longrightarrow> ns n = a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> n < Suc k

goal (1 subgoal):
 1. \<not> n < Suc k \<Longrightarrow> ns n = a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> n < Suc k

goal (1 subgoal):
 1. ns n = a
[PROOF STEP]
using A Suc.IH True
[PROOF STATE]
proof (prove)
using this:
\<not> n < Suc k
n \<le> Suc k
\<forall>n\<le>k. ns n = a
ns 1 = a

goal (1 subgoal):
 1. ns n = a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ns n = a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns n = a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n\<le>Suc k. ns n = a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n\<le>k. ns n = a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n\<le>?k2. ns n = a

goal (2 subgoals):
 1. ns 1 = a \<Longrightarrow> val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
 2. ns 1 \<noteq> a \<Longrightarrow> val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
show "val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f\<bullet>a) (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
by (metis T0  Zp_def Zp_defs(3) f'a_closed f'a_nonzero fa_nonzero
              hensel.fa_closed hensel_axioms hensel_hypothesis_weakened le_eq_less_or_eq
              newton_seq_fact9 not_nonzero_Qp order_less_le val_of_divide)
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. ns 1 \<noteq> a \<Longrightarrow> val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns 1 \<noteq> a \<Longrightarrow> val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
ns 1 \<noteq> a

goal (1 subgoal):
 1. ns 1 \<noteq> a \<Longrightarrow> val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have F0: "(1::nat) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> n
[PROOF STEP]
using AA
[PROOF STATE]
proof (prove)
using this:
1 < n

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

goal (1 subgoal):
 1. ns 1 \<noteq> a \<Longrightarrow> val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have "(f\<bullet>a) \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> a \<noteq> \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f \<bullet> a \<noteq> \<zero>

goal (1 subgoal):
 1. ns 1 \<noteq> a \<Longrightarrow> val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have "\<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f\<bullet>a) (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
show " val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f\<bullet>a) (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
proof(induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. val_Zp (a \<ominus> ns (Suc 0)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
 2. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. val_Zp (a \<ominus> ns (Suc 0)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
 2. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have "(a \<ominus> ns (Suc 0)) = (local.divide (f\<bullet>a) (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<ominus> ns (Suc 0) = local.divide (f \<bullet> a) (f' \<bullet> a)
[PROOF STEP]
by (metis R.minus_minus Zp_def hensel.newton_seq_fact7 hensel_axioms
                  local.a_closed minus_a_inv newton_seq.simps(1) newton_seq.simps(2) newton_seq_fact5 newton_step_closed)
[PROOF STATE]
proof (state)
this:
a \<ominus> ns (Suc 0) = local.divide (f \<bullet> a) (f' \<bullet> a)

goal (2 subgoals):
 1. val_Zp (a \<ominus> ns (Suc 0)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
 2. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<ominus> ns (Suc 0) = local.divide (f \<bullet> a) (f' \<bullet> a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<ominus> ns (Suc 0) = local.divide (f \<bullet> a) (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (a \<ominus> ns (Suc 0)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> ns (Suc 0)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have I0: "ns (Suc (Suc k)) = ns (Suc k) \<ominus> (divide (f\<bullet>(ns (Suc k))) (f'\<bullet>(ns (Suc k))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns (Suc (Suc k)) = ns (Suc k) \<ominus> local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k))
[PROOF STEP]
by (simp add: newton_step_def)
[PROOF STATE]
proof (state)
this:
ns (Suc (Suc k)) = ns (Suc k) \<ominus> local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k))

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have I1: "val_Zp (f\<bullet>(ns (Suc k))) \<ge> val_Zp(f'\<bullet>(ns (Suc k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns (Suc k)) \<le> val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
using newton_seq_fact3
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns ?l) \<le> val_Zp (f \<bullet> ns ?l)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns (Suc k)) \<le> val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns (Suc k)) \<le> val_Zp (f \<bullet> ns (Suc k))

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have I2: "(divide (f\<bullet>(ns (Suc k))) (f'\<bullet>(ns (Suc k)))) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k)) \<in> carrier Zp
[PROOF STEP]
using newton_seq_fact5
[PROOF STATE]
proof (prove)
using this:
local.divide (f \<bullet> ns ?l) (f' \<bullet> ns ?l) \<in> carrier Zp

goal (1 subgoal):
 1. local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k)) \<in> carrier Zp
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k)) \<in> carrier Zp

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have I3: "ns (Suc (Suc k)) \<ominus> ns (Suc k) = \<ominus>(divide (f\<bullet>(ns (Suc k))) (f'\<bullet>(ns (Suc k))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns (Suc (Suc k)) \<ominus> ns (Suc k) = \<ominus> local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k))
[PROOF STEP]
using I0 I2 newton_seq_fact7
[PROOF STATE]
proof (prove)
using this:
ns (Suc (Suc k)) = ns (Suc k) \<ominus> local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k))
local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k)) \<in> carrier Zp
ns (Suc ?n) \<ominus> ns ?n = \<ominus> local.divide (f \<bullet> ns ?n) (f' \<bullet> ns ?n)

goal (1 subgoal):
 1. ns (Suc (Suc k)) \<ominus> ns (Suc k) = \<ominus> local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns (Suc (Suc k)) \<ominus> ns (Suc k) = \<ominus> local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k))

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ns (Suc (Suc k)) \<ominus> ns (Suc k) = \<ominus> local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k))
[PROOF STEP]
have "val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (divide (f\<bullet>(ns (Suc k))) (f'\<bullet>(ns (Suc k))))"
[PROOF STATE]
proof (prove)
using this:
ns (Suc (Suc k)) \<ominus> ns (Suc k) = \<ominus> local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k))

goal (1 subgoal):
 1. val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k)))
[PROOF STEP]
using I2 val_Zp_of_minus
[PROOF STATE]
proof (prove)
using this:
ns (Suc (Suc k)) \<ominus> ns (Suc k) = \<ominus> local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k))
local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k)) \<in> carrier Zp
?a \<in> carrier Zp \<Longrightarrow> val_Zp ?a = val_Zp (\<ominus> ?a)

goal (1 subgoal):
 1. val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k)))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k)))

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k)))
[PROOF STEP]
have "val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (f\<bullet>(ns (Suc k))) - val_Zp (f'\<bullet>(ns (Suc k)))"
[PROOF STATE]
proof (prove)
using this:
val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> ns (Suc k)) (f' \<bullet> ns (Suc k)))

goal (1 subgoal):
 1. val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (f \<bullet> ns (Suc k)) - val_Zp (f' \<bullet> ns (Suc k))
[PROOF STEP]
by (metis I1 R.zero_closed Zp_def newton_seq_fact6 newton_seq_fact9 padic_integers.val_of_divide padic_integers_axioms)
[PROOF STATE]
proof (state)
this:
val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (f \<bullet> ns (Suc k)) - val_Zp (f' \<bullet> ns (Suc k))

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (f \<bullet> ns (Suc k)) - val_Zp (f' \<bullet> ns (Suc k))
[PROOF STEP]
have I4: "val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (f\<bullet>(ns (Suc k))) - val_Zp ((f'\<bullet>a))"
[PROOF STATE]
proof (prove)
using this:
val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (f \<bullet> ns (Suc k)) - val_Zp (f' \<bullet> ns (Suc k))

goal (1 subgoal):
 1. val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (f \<bullet> ns (Suc k)) - val_Zp (f' \<bullet> a)
[PROOF STEP]
using newton_seq_fact1
[PROOF STATE]
proof (prove)
using this:
val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (f \<bullet> ns (Suc k)) - val_Zp (f' \<bullet> ns (Suc k))
val_Zp (f' \<bullet> ns ?k) = val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (f \<bullet> ns (Suc k)) - val_Zp (f' \<bullet> a)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
val_Zp (ns (Suc (Suc k)) \<ominus> ns (Suc k)) = val_Zp (f \<bullet> ns (Suc k)) - val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have F3: "val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f\<bullet>a) (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
using Suc.IH
[PROOF STATE]
proof (prove)
using this:
val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have F4: "a \<ominus>  ns (Suc (Suc k)) = (a \<ominus> ( ns (Suc k))) \<oplus> (ns  (Suc k)) \<ominus> ns (Suc (Suc k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<ominus> ns (Suc (Suc k)) = a \<ominus> ns (Suc k) \<oplus> ns (Suc k) \<ominus> ns (Suc (Suc k))
[PROOF STEP]
by (metis R.ring_simprules(17) a_minus_def add_comm local.a_closed newton_seq_closed)
[PROOF STATE]
proof (state)
this:
a \<ominus> ns (Suc (Suc k)) = a \<ominus> ns (Suc k) \<oplus> ns (Suc k) \<ominus> ns (Suc (Suc k))

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have F5: "val_Zp ((ns  (Suc k)) \<ominus> ns (Suc (Suc k))) > val_Zp (a \<ominus> ( ns (Suc k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (a \<ominus> ns (Suc k)) < val_Zp (ns (Suc k) \<ominus> ns (Suc (Suc k)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (a \<ominus> ns (Suc k)) < val_Zp (ns (Suc k) \<ominus> ns (Suc (Suc k)))
[PROOF STEP]
have F50:  "val_Zp ((ns  (Suc k)) \<ominus> ns (Suc (Suc k))) = val_Zp (f\<bullet>(ns (Suc k))) - val_Zp ((f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (ns (Suc k) \<ominus> ns (Suc (Suc k))) = val_Zp (f \<bullet> ns (Suc k)) - val_Zp (f' \<bullet> a)
[PROOF STEP]
by (metis I4 R.minus_closed minus_a_inv newton_seq_closed val_Zp_of_minus)
[PROOF STATE]
proof (state)
this:
val_Zp (ns (Suc k) \<ominus> ns (Suc (Suc k))) = val_Zp (f \<bullet> ns (Suc k)) - val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (a \<ominus> ns (Suc k)) < val_Zp (ns (Suc k) \<ominus> ns (Suc (Suc k)))
[PROOF STEP]
have F51: "val_Zp (f\<bullet>(ns (Suc k))) > val_Zp ((f\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f \<bullet> a) < val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f \<bullet> a) < val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
have F510: "val_Zp (f\<bullet>(ns (Suc k))) \<ge>  2*val_Zp (f'\<bullet>a) + 2^(Suc k)*t "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ Suc k) * t \<le> val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
using newton_seq_fact2
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k) * t \<le> val_Zp (f \<bullet> ns ?k)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ Suc k) * t \<le> val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ Suc k) * t \<le> val_Zp (f \<bullet> ns (Suc k))

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) < val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
hence F511: "val_Zp (f\<bullet>(ns (Suc k))) \<ge>  2*val_Zp (f'\<bullet>a) + 2*t "
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ Suc k) * t \<le> val_Zp (f \<bullet> ns (Suc k))

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t \<le> val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
using eint_plus_times[of t "2*val_Zp (f'\<bullet>a)" "2^(Suc k)" "val_Zp (f\<bullet>(ns (Suc k)))" 2] t_pos
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ Suc k) * t \<le> val_Zp (f \<bullet> ns (Suc k))
\<lbrakk>0 \<le> t; eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ Suc k) * t \<le> val_Zp (f \<bullet> ns (Suc k)); 2 \<le> 2 ^ Suc k\<rbrakk> \<Longrightarrow> eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t \<le> val_Zp (f \<bullet> ns (Suc k))
0 < t

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t \<le> val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
by (simp add: order_less_le)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t \<le> val_Zp (f \<bullet> ns (Suc k))

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) < val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
have F512: "2*val_Zp (f'\<bullet>a) + 2*t  = 2 *val_Zp (f\<bullet>a) - 2* val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t = eint 2 * val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
[PROOF STEP]
unfolding hensel_factor_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint 2 * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) = eint 2 * val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
[PROOF STEP]
using eint_minus_distr[of "val_Zp (f\<bullet>a)" "2 * val_Zp (f'\<bullet>a)" 2]
                        eint_minus_comm[of _ _ "eint 2 * (eint 2 * val_Zp (f'\<bullet>a))"]
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> a) \<noteq> eint 2 * val_Zp (f' \<bullet> a) \<Longrightarrow> eint 2 * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) = eint 2 * val_Zp (f \<bullet> a) - eint 2 * (eint 2 * val_Zp (f' \<bullet> a))
?d + ?b - eint 2 * (eint 2 * val_Zp (f' \<bullet> a)) = ?d - eint 2 * (eint 2 * val_Zp (f' \<bullet> a)) + ?b

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint 2 * (val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)) = eint 2 * val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
[PROOF STEP]
by (smt eint_2_minus_1_mult eint_add_cancel_fact eint_minus_comm f'a_not_infinite hensel_hypothesis nat_mult_not_infty order_less_le)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t = eint 2 * val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) < val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
hence "2*val_Zp (f'\<bullet>a) + 2*t  > val_Zp (f\<bullet>a)"
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t = eint 2 * val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) < eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t
[PROOF STEP]
using hensel_hypothesis
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t = eint 2 * val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
eint 2 * val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) < eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t
[PROOF STEP]
by (smt add_diff_cancel_eint eint_add_cancel_fact eint_add_left_cancel_le
                      eint_pos_int_times_gt f'a_not_infinite hensel_factor_def nat_mult_not_infty order_less_le t_neq_infty t_pos)
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> a) < eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) < val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> a) < eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) < val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
using F512
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> a) < eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t
eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t = eint 2 * val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) < val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
using F511 less_le_trans
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> a) < eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t
eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t = eint 2 * val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
eint 2 * val_Zp (f' \<bullet> a) + eint 2 * t \<le> val_Zp (f \<bullet> ns (Suc k))
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. val_Zp (f \<bullet> a) < val_Zp (f \<bullet> ns (Suc k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> a) < val_Zp (f \<bullet> ns (Suc k))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> a) < val_Zp (f \<bullet> ns (Suc k))

goal (1 subgoal):
 1. val_Zp (a \<ominus> ns (Suc k)) < val_Zp (ns (Suc k) \<ominus> ns (Suc (Suc k)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> a) < val_Zp (f \<bullet> ns (Suc k))

goal (1 subgoal):
 1. val_Zp (a \<ominus> ns (Suc k)) < val_Zp (ns (Suc k) \<ominus> ns (Suc (Suc k)))
[PROOF STEP]
by (metis F3 F50 Zp_def divide_closed eint_add_cancel_fact eint_minus_ineq
                    f'a_closed f'a_nonzero f'a_not_infinite fa_closed fa_nonzero hensel.newton_seq_fact7
                    hensel_axioms newton_seq.simps(1) newton_seq_fact9 order_less_le val_Zp_of_minus)
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> ns (Suc k)) < val_Zp (ns (Suc k) \<ominus> ns (Suc (Suc k)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> ns (Suc k)) < val_Zp (ns (Suc k) \<ominus> ns (Suc (Suc k)))

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have "a \<ominus> ns (Suc k) \<oplus> (ns (Suc k) \<ominus> ns (Suc (Suc k))) = a  \<ominus> ns (Suc (Suc k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<ominus> ns (Suc k) \<oplus> (ns (Suc k) \<ominus> ns (Suc (Suc k))) = a \<ominus> ns (Suc (Suc k))
[PROOF STEP]
by (metis F4 a_minus_def add_assoc)
[PROOF STATE]
proof (state)
this:
a \<ominus> ns (Suc k) \<oplus> (ns (Suc k) \<ominus> ns (Suc (Suc k))) = a \<ominus> ns (Suc (Suc k))

goal (1 subgoal):
 1. \<And>k. val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<ominus> ns (Suc k) \<oplus> (ns (Suc k) \<ominus> ns (Suc (Suc k))) = a \<ominus> ns (Suc (Suc k))
[PROOF STEP]
show F6: "val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f\<bullet>a) (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
using this:
a \<ominus> ns (Suc k) \<oplus> (ns (Suc k) \<ominus> ns (Suc (Suc k))) = a \<ominus> ns (Suc (Suc k))

goal (1 subgoal):
 1. val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
using F5 F4 F3
[PROOF STATE]
proof (prove)
using this:
a \<ominus> ns (Suc k) \<oplus> (ns (Suc k) \<ominus> ns (Suc (Suc k))) = a \<ominus> ns (Suc (Suc k))
val_Zp (a \<ominus> ns (Suc k)) < val_Zp (ns (Suc k) \<ominus> ns (Suc (Suc k)))
a \<ominus> ns (Suc (Suc k)) = a \<ominus> ns (Suc k) \<oplus> ns (Suc k) \<ominus> ns (Suc (Suc k))
val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
by (metis R.minus_closed local.a_closed newton_seq_closed order_less_le val_Zp_not_equal_ord_plus_minus val_Zp_ultrametric_eq'')
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> ns (Suc (Suc k))) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> ns (Suc k)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> ns (Suc ?k2)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. ns 1 \<noteq> a \<Longrightarrow> val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp (a \<ominus> ns (Suc ?k2)) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
by (metis AA less_imp_add_positive plus_1_eq_Suc)
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 < ?m2 \<Longrightarrow> val_Zp (a \<ominus> ns ?m2) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. \<exists>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 < ?m2 \<Longrightarrow> val_Zp (a \<ominus> ns ?m2) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. \<exists>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hensel_seq_comp_f:
 "res_lim ((to_fun f) \<circ> ns) = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. res_lim ((\<bullet>) f \<circ> ns) = \<zero>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. res_lim ((\<bullet>) f \<circ> ns) = \<zero>
[PROOF STEP]
have A: "is_Zp_cauchy ((to_fun f) \<circ> ns)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_Zp_cauchy ((\<bullet>) f \<circ> ns)
[PROOF STEP]
using f_closed is_Zp_continuous_def newton_seq_is_Zp_cauchy polynomial_is_Zp_continuous
[PROOF STATE]
proof (prove)
using this:
f \<in> carrier (UP Zp)
is_Zp_continuous ?f = (?f \<in> carrier (function_ring (carrier Zp) Zp) \<and> (\<forall>s. is_Zp_cauchy s \<longrightarrow> is_Zp_cauchy (?f \<circ> s)))
is_Zp_cauchy ns
?f \<in> carrier (UP Zp) \<Longrightarrow> is_Zp_continuous ((\<bullet>) ?f)

goal (1 subgoal):
 1. is_Zp_cauchy ((\<bullet>) f \<circ> ns)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_Zp_cauchy ((\<bullet>) f \<circ> ns)

goal (1 subgoal):
 1. res_lim ((\<bullet>) f \<circ> ns) = \<zero>
[PROOF STEP]
have "Zp_converges_to ((to_fun f) \<circ> ns) \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Zp_converges_to ((\<bullet>) f \<circ> ns) \<zero>
[PROOF STEP]
apply(rule Zp_converges_toI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<bullet>) f \<circ> ns \<in> carrier Zp\<^bsup>\<omega>\<^esup>
 2. \<zero> \<in> carrier Zp
 3. \<And>n. \<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
using A is_Zp_cauchy_def
[PROOF STATE]
proof (prove)
using this:
is_Zp_cauchy ((\<bullet>) f \<circ> ns)
is_Zp_cauchy ?s = (?s \<in> carrier Zp\<^bsup>\<omega>\<^esup> \<and> (\<forall>n. \<exists>N. \<forall>m k. N < m \<and> N < k \<longrightarrow> eint n < val_Zp_dist (?s m) (?s k)))

goal (3 subgoals):
 1. (\<bullet>) f \<circ> ns \<in> carrier Zp\<^bsup>\<omega>\<^esup>
 2. \<zero> \<in> carrier Zp
 3. \<And>n. \<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<zero> \<in> carrier Zp
 2. \<And>n. \<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
show " \<exists>N. \<forall>k>N. (((to_fun f) \<circ> ns) k) n = \<zero> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
have 0: "\<And>k. (k::nat)>3 \<longrightarrow>  val_Zp (f\<bullet>(ns k)) > k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. 3 < k \<longrightarrow> eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. 3 < k \<Longrightarrow> eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
fix k::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. 3 < k \<Longrightarrow> eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
assume A: "k >3"
[PROOF STATE]
proof (state)
this:
3 < k

goal (1 subgoal):
 1. \<And>k. 3 < k \<Longrightarrow> eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
show "val_Zp (f\<bullet>(ns k)) > k "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
have 0: " val_Zp (f\<bullet>(ns k)) \<ge>  2*(val_Zp (f'\<bullet>a)) + (2^k)*t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
using newton_seq_fact2
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ ?k) * t \<le> val_Zp (f \<bullet> ns ?k)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
have 1: "2*(val_Zp (f'\<bullet>a)) + (2^k)*t > k "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
[PROOF STEP]
have "(2^k)*t \<ge> (2^k) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint (2 ^ k) \<le> eint (2 ^ k) * t
[PROOF STEP]
apply(cases "t = \<infinity>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. t = \<infinity> \<Longrightarrow> eint (2 ^ k) \<le> eint (2 ^ k) * t
 2. t \<noteq> \<infinity> \<Longrightarrow> eint (2 ^ k) \<le> eint (2 ^ k) * t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<noteq> \<infinity> \<Longrightarrow> eint (2 ^ k) \<le> eint (2 ^ k) * t
[PROOF STEP]
using t_pos eint_mult_mono'
[PROOF STATE]
proof (prove)
using this:
0 < t
\<lbrakk>0 \<le> ?c \<and> ?c \<noteq> \<infinity>; ?n < ?k\<rbrakk> \<Longrightarrow> ?n * ?c \<le> ?k * ?c

goal (1 subgoal):
 1. t \<noteq> \<infinity> \<Longrightarrow> eint (2 ^ k) \<le> eint (2 ^ k) * t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>t \<noteq> \<infinity>; 0 < t; \<And>c n k. \<lbrakk>0 \<le> c \<and> c \<noteq> \<infinity>; n < k\<rbrakk> \<Longrightarrow> n * c \<le> k * c\<rbrakk> \<Longrightarrow> eint (2 ^ k) \<le> eint (2 ^ k) * t
[PROOF STEP]
obtain ii :: "eint \<Rightarrow> int" where
                f1: "\<forall>e. (\<infinity> \<noteq> e \<or> (\<forall>i. eint i \<noteq> e)) \<and> (eint (ii e) = e \<or> \<infinity> = e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ii. \<forall>e. (\<infinity> \<noteq> e \<or> (\<forall>i. eint i \<noteq> e)) \<and> (eint (ii e) = e \<or> \<infinity> = e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis not_infinity_eq)
[PROOF STATE]
proof (state)
this:
\<forall>e. (\<infinity> \<noteq> e \<or> (\<forall>i. eint i \<noteq> e)) \<and> (eint (ii e) = e \<or> \<infinity> = e)

goal (1 subgoal):
 1. \<lbrakk>t \<noteq> \<infinity>; 0 < t; \<And>c n k. \<lbrakk>0 \<le> c \<and> c \<noteq> \<infinity>; n < k\<rbrakk> \<Longrightarrow> n * c \<le> k * c\<rbrakk> \<Longrightarrow> eint (2 ^ k) \<le> eint (2 ^ k) * t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>e. (\<infinity> \<noteq> e \<or> (\<forall>i. eint i \<noteq> e)) \<and> (eint (ii e) = e \<or> \<infinity> = e)
[PROOF STEP]
have "0 < ii t"
[PROOF STATE]
proof (prove)
using this:
\<forall>e. (\<infinity> \<noteq> e \<or> (\<forall>i. eint i \<noteq> e)) \<and> (eint (ii e) = e \<or> \<infinity> = e)

goal (1 subgoal):
 1. 0 < ii t
[PROOF STEP]
by (metis (no_types) eint_ord_simps(2) t_neq_infty t_pos zero_eint_def)
[PROOF STATE]
proof (state)
this:
0 < ii t

goal (1 subgoal):
 1. \<lbrakk>t \<noteq> \<infinity>; 0 < t; \<And>c n k. \<lbrakk>0 \<le> c \<and> c \<noteq> \<infinity>; n < k\<rbrakk> \<Longrightarrow> n * c \<le> k * c\<rbrakk> \<Longrightarrow> eint (2 ^ k) \<le> eint (2 ^ k) * t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ii t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < ii t

goal (1 subgoal):
 1. eint (2 ^ k) \<le> eint (2 ^ k) * t
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
0 < ii t
\<forall>e. (\<infinity> \<noteq> e \<or> (\<forall>i. eint i \<noteq> e)) \<and> (eint (ii e) = e \<or> \<infinity> = e)

goal (1 subgoal):
 1. eint (2 ^ k) \<le> eint (2 ^ k) * t
[PROOF STEP]
by (metis eint_pos_int_times_ge eint_mult_mono linorder_not_less
                            mult.commute order_less_le t_neq_infty t_pos t_times_pow_pos)
[PROOF STATE]
proof (state)
this:
eint (2 ^ k) \<le> eint (2 ^ k) * t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint (2 ^ k) \<le> eint (2 ^ k) * t

goal (1 subgoal):
 1. eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
[PROOF STEP]
hence " 2*(val_Zp (f'\<bullet>a)) + (2^k)*t \<ge> (2^k) "
[PROOF STATE]
proof (prove)
using this:
eint (2 ^ k) \<le> eint (2 ^ k) * t

goal (1 subgoal):
 1. eint (2 ^ k) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
[PROOF STEP]
by (smt Groups.add_ac(2) add.right_neutral eint_2_minus_1_mult eint_pos_times_is_pos
                  eint_pow_int_is_pos f'a_nonneg_val ge_plus_pos_imp_gt idiff_0_right linorder_not_less
                  nat_mult_not_infty order_less_le t_neq_infty)
[PROOF STATE]
proof (state)
this:
eint (2 ^ k) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t

goal (1 subgoal):
 1. eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint (2 ^ k) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
[PROOF STEP]
have  " 2*(val_Zp (f'\<bullet>a)) + (2^k)*t > k"
[PROOF STATE]
proof (prove)
using this:
eint (2 ^ k) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t

goal (1 subgoal):
 1. eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
[PROOF STEP]
using A  of_nat_1 of_nat_add of_nat_less_two_power
[PROOF STATE]
proof (prove)
using this:
eint (2 ^ k) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
3 < k
of_nat 1 = (1::?'a)
of_nat (?m + ?n) = of_nat ?m + of_nat ?n
of_nat ?n < (2::?'a) ^ ?n

goal (1 subgoal):
 1. eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
[PROOF STEP]
by (smt eint_ord_simps(1) linorder_not_less order_trans)
[PROOF STATE]
proof (state)
this:
eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t

goal (1 subgoal):
 1. eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t

goal (1 subgoal):
 1. eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t

goal (1 subgoal):
 1. eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t

goal (1 subgoal):
 1. eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
using 0 less_le_trans
[PROOF STATE]
proof (prove)
using this:
eint (int k) < eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ k) * t \<le> val_Zp (f \<bullet> ns k)
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eint (int k) < val_Zp (f \<bullet> ns k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint (int k) < val_Zp (f \<bullet> ns k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
3 < ?k2 \<longrightarrow> eint (int ?k2) < val_Zp (f \<bullet> ns ?k2)

goal (1 subgoal):
 1. \<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
have 1: "\<And>k. (k::nat)>3 \<longrightarrow>  (f\<bullet>(ns k)) k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. 3 < k \<longrightarrow> (f \<bullet> ns k) k = 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. 3 < k \<Longrightarrow> (f \<bullet> ns k) k = 0
[PROOF STEP]
fix k::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. 3 < k \<Longrightarrow> (f \<bullet> ns k) k = 0
[PROOF STEP]
assume B: "3<k"
[PROOF STATE]
proof (state)
this:
3 < k

goal (1 subgoal):
 1. \<And>k. 3 < k \<Longrightarrow> (f \<bullet> ns k) k = 0
[PROOF STEP]
show " (f\<bullet>(ns k)) k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<bullet> ns k) k = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f \<bullet> ns k) k = 0
[PROOF STEP]
have B0: " val_Zp (f\<bullet>(ns k)) > k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
using 0 B
[PROOF STATE]
proof (prove)
using this:
3 < ?k2 \<longrightarrow> eint (int ?k2) < val_Zp (f \<bullet> ns ?k2)
3 < k

goal (1 subgoal):
 1. eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eint (int k) < val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. (f \<bullet> ns k) k = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint (int k) < val_Zp (f \<bullet> ns k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eint (int k) < val_Zp (f \<bullet> ns k)

goal (1 subgoal):
 1. (f \<bullet> ns k) k = 0
[PROOF STEP]
by (simp add: f_of_newton_seq_closed zero_below_val_Zp)
[PROOF STATE]
proof (state)
this:
(f \<bullet> ns k) k = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(f \<bullet> ns k) k = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
3 < ?k2 \<longrightarrow> (f \<bullet> ns ?k2) ?k2 = 0

goal (1 subgoal):
 1. \<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
have "\<forall>k>(max 3 n). (((to_fun f) \<circ> ns) k) n = \<zero> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k>max 3 n. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>3 < k; n < k\<rbrakk> \<Longrightarrow> (f \<bullet> ns k) n = \<zero> n
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>3 < k; n < k\<rbrakk> \<Longrightarrow> (f \<bullet> ns k) n = \<zero> n
[PROOF STEP]
fix k::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>3 < k; n < k\<rbrakk> \<Longrightarrow> (f \<bullet> ns k) n = \<zero> n
[PROOF STEP]
assume A: "3< k"
[PROOF STATE]
proof (state)
this:
3 < k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>3 < k; n < k\<rbrakk> \<Longrightarrow> (f \<bullet> ns k) n = \<zero> n
[PROOF STEP]
assume A': "n < k"
[PROOF STATE]
proof (state)
this:
n < k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>3 < k; n < k\<rbrakk> \<Longrightarrow> (f \<bullet> ns k) n = \<zero> n
[PROOF STEP]
have A0: "(f\<bullet>(ns k)) k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<bullet> ns k) k = 0
[PROOF STEP]
using 1[of k] A
[PROOF STATE]
proof (prove)
using this:
3 < k \<longrightarrow> (f \<bullet> ns k) k = 0
3 < k

goal (1 subgoal):
 1. (f \<bullet> ns k) k = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f \<bullet> ns k) k = 0

goal (1 subgoal):
 1. \<And>k. \<lbrakk>3 < k; n < k\<rbrakk> \<Longrightarrow> (f \<bullet> ns k) n = \<zero> n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(f \<bullet> ns k) k = 0
[PROOF STEP]
have "(f\<bullet>(ns k)) n = 0"
[PROOF STATE]
proof (prove)
using this:
(f \<bullet> ns k) k = 0

goal (1 subgoal):
 1. (f \<bullet> ns k) n = 0
[PROOF STEP]
using A A'
[PROOF STATE]
proof (prove)
using this:
(f \<bullet> ns k) k = 0
3 < k
n < k

goal (1 subgoal):
 1. (f \<bullet> ns k) n = 0
[PROOF STEP]
using above_ord_nonzero[of "(f\<bullet>(ns k))"]
[PROOF STATE]
proof (prove)
using this:
(f \<bullet> ns k) k = 0
3 < k
n < k
\<lbrakk>f \<bullet> ns k \<in> carrier Zp; f \<bullet> ns k \<noteq> \<zero>; ord_Zp (f \<bullet> ns k) < int ?n\<rbrakk> \<Longrightarrow> (f \<bullet> ns k) ?n \<noteq> 0

goal (1 subgoal):
 1. (f \<bullet> ns k) n = 0
[PROOF STEP]
by (smt UP_cring.to_fun_closed Zp_x_is_UP_cring f_closed le_eq_less_or_eq
              newton_seq_closed of_nat_mono residue_of_zero(2) zero_below_ord)
[PROOF STATE]
proof (state)
this:
(f \<bullet> ns k) n = 0

goal (1 subgoal):
 1. \<And>k. \<lbrakk>3 < k; n < k\<rbrakk> \<Longrightarrow> (f \<bullet> ns k) n = \<zero> n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(f \<bullet> ns k) n = 0
[PROOF STEP]
show A1:  "to_fun f (ns k) n = \<zero> n"
[PROOF STATE]
proof (prove)
using this:
(f \<bullet> ns k) n = 0

goal (1 subgoal):
 1. (f \<bullet> ns k) n = \<zero> n
[PROOF STEP]
by (simp add: residue_of_zero(2))
[PROOF STATE]
proof (state)
this:
(f \<bullet> ns k) n = \<zero> n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k>max 3 n. ((\<bullet>) f \<circ> ns) k n = \<zero> n

goal (1 subgoal):
 1. \<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>k>max 3 n. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>k>max 3 n. ((\<bullet>) f \<circ> ns) k n = \<zero> n

goal (1 subgoal):
 1. \<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>N. \<forall>k>N. ((\<bullet>) f \<circ> ns) k n = \<zero> n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Zp_converges_to ((\<bullet>) f \<circ> ns) \<zero>

goal (1 subgoal):
 1. res_lim ((\<bullet>) f \<circ> ns) = \<zero>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Zp_converges_to ((\<bullet>) f \<circ> ns) \<zero>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Zp_converges_to ((\<bullet>) f \<circ> ns) \<zero>

goal (1 subgoal):
 1. res_lim ((\<bullet>) f \<circ> ns) = \<zero>
[PROOF STEP]
by (metis Zp_converges_to_def unique_limit')
[PROOF STATE]
proof (state)
this:
res_lim ((\<bullet>) f \<circ> ns) = \<zero>

goal:
No subgoals!
[PROOF STEP]
qed