[STATEMENT]
lemma full_hensels_lemma:
  obtains \<alpha> where
       "f\<bullet>\<alpha> = \<zero>" and "\<alpha> \<in> carrier Zp"
       "val_Zp (a \<ominus> \<alpha>) > val_Zp (f'\<bullet>a)"
       "(val_Zp (a \<ominus> \<alpha>) = val_Zp (divide (f\<bullet>a) (f'\<bullet>a)))"
       "val_Zp (f'\<bullet>\<alpha>) = val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(cases "\<exists>k. f\<bullet>(ns k) =\<zero>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<exists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>k. f \<bullet> ns k = \<zero>

goal (2 subgoals):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<exists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain k where k_def: "f\<bullet>(ns k) =\<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. f \<bullet> ns k = \<zero> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
\<exists>k. f \<bullet> ns k = \<zero>

goal (1 subgoal):
 1. (\<And>k. f \<bullet> ns k = \<zero> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<bullet> ns k = \<zero>

goal (2 subgoals):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<exists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain N where N_def: "\<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. (\<And>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pre_hensel(2)
[PROOF STATE]
proof (prove)
using this:
\<exists>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

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

goal (2 subgoals):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<exists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have Z: "\<And>n. n \<ge>k \<Longrightarrow> f\<bullet>(ns n) =\<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. k \<le> n \<Longrightarrow> f \<bullet> ns n = \<zero>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. k \<le> n \<Longrightarrow> f \<bullet> ns n = \<zero>
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. k \<le> n \<Longrightarrow> f \<bullet> ns n = \<zero>
[PROOF STEP]
assume A: "n \<ge>k"
[PROOF STATE]
proof (state)
this:
k \<le> n

goal (1 subgoal):
 1. \<And>n. k \<le> n \<Longrightarrow> f \<bullet> ns n = \<zero>
[PROOF STEP]
obtain l where l_def:"n = k + l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. n = k + l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A le_Suc_ex
[PROOF STATE]
proof (prove)
using this:
k \<le> n
?k \<le> ?l \<Longrightarrow> \<exists>n. ?l = ?k + n

goal (1 subgoal):
 1. (\<And>l. n = k + l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n = k + l

goal (1 subgoal):
 1. \<And>n. k \<le> n \<Longrightarrow> f \<bullet> ns n = \<zero>
[PROOF STEP]
have "\<And>m. f\<bullet>(ns (k+m)) =\<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. f \<bullet> ns (k + m) = \<zero>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. f \<bullet> ns (k + m) = \<zero>
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. f \<bullet> ns (k + m) = \<zero>
[PROOF STEP]
show "f\<bullet>(ns (k+m)) =\<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> ns (k + m) = \<zero>
[PROOF STEP]
apply(induction m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. f \<bullet> ns (k + 0) = \<zero>
 2. \<And>m. f \<bullet> ns (k + m) = \<zero> \<Longrightarrow> f \<bullet> ns (k + Suc m) = \<zero>
[PROOF STEP]
apply (simp add: k_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. f \<bullet> ns (k + m) = \<zero> \<Longrightarrow> f \<bullet> ns (k + Suc m) = \<zero>
[PROOF STEP]
using  eventually_zero
[PROOF STATE]
proof (prove)
using this:
f \<bullet> ns (?k + ?m) = \<zero> \<Longrightarrow> f \<bullet> ns (?k + Suc ?m) = \<zero>

goal (1 subgoal):
 1. \<And>m. f \<bullet> ns (k + m) = \<zero> \<Longrightarrow> f \<bullet> ns (k + Suc m) = \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f \<bullet> ns (k + m) = \<zero>

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

goal (1 subgoal):
 1. \<And>n. k \<le> n \<Longrightarrow> f \<bullet> ns n = \<zero>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<bullet> ns (k + ?m2) = \<zero>
[PROOF STEP]
show "f\<bullet>(ns n) =\<zero>"
[PROOF STATE]
proof (prove)
using this:
f \<bullet> ns (k + ?m2) = \<zero>

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

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

goal (2 subgoals):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<exists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain M where M_def: "M = N + k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>M. M = N + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
M = N + k

goal (2 subgoals):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<exists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M = N + k
[PROOF STEP]
have M_root: "f\<bullet>(ns M) =\<zero>"
[PROOF STATE]
proof (prove)
using this:
M = N + k

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

goal (2 subgoals):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<exists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain \<alpha> where alpha_def: "\<alpha>= ns M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha>. \<alpha> = ns M \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<alpha> = ns M

goal (2 subgoals):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<exists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have T0: "f\<bullet>\<alpha> = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> \<alpha> = \<zero>
[PROOF STEP]
using alpha_def M_root
[PROOF STATE]
proof (prove)
using this:
\<alpha> = ns M
f \<bullet> ns M = \<zero>

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

goal (2 subgoals):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<exists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have T1:    "val_Zp (a \<ominus> \<alpha>) > val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
using alpha_def pre_hensel(1)
[PROOF STATE]
proof (prove)
using this:
\<alpha> = ns M
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns ?n)

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

goal (2 subgoals):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<exists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have T2: "(val_Zp (a \<ominus> \<alpha>) = val_Zp (divide (f\<bullet>a) (f'\<bullet>a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
by (metis M_def N_def alpha_def fa_nonzero k_def
        less_add_same_cancel1 newton_seq.elims zero_less_Suc)
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (2 subgoals):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<exists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have T3:  "val_Zp (f'\<bullet>\<alpha>) = val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)
[PROOF STEP]
using alpha_def newton_seq_fact1
[PROOF STATE]
proof (prove)
using this:
\<alpha> = ns M
val_Zp (f' \<bullet> ns ?k) = val_Zp (f' \<bullet> a)

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

goal (2 subgoals):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<exists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using T0 T1 T2 T3
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<alpha> = \<zero>
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that alpha_def newton_seq_closed
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<alpha> = \<zero>
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)
\<lbrakk>f \<bullet> ?\<alpha>2 = \<zero>; ?\<alpha>2 \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ?\<alpha>2); val_Zp (a \<ominus> ?\<alpha>2) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> ?\<alpha>2) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis
\<alpha> = ns M
ns ?m \<in> carrier Zp

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>k. f \<bullet> ns k = \<zero>

goal (1 subgoal):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>k. f \<bullet> ns k = \<zero>
[PROOF STEP]
have Nz: "\<And>k. f\<bullet>(ns k) \<noteq>\<zero>"
[PROOF STATE]
proof (prove)
using this:
\<nexists>k. f \<bullet> ns k = \<zero>

goal (1 subgoal):
 1. \<And>k. f \<bullet> ns k \<noteq> \<zero>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<bullet> ns ?k2 \<noteq> \<zero>

goal (1 subgoal):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have ns_cauchy: "is_Zp_cauchy ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_Zp_cauchy ns
[PROOF STEP]
by (simp add: newton_seq_is_Zp_cauchy)
[PROOF STATE]
proof (state)
this:
is_Zp_cauchy ns

goal (1 subgoal):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have fns_cauchy: "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 ns_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. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have F0: "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]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. res_lim ((\<bullet>) f \<circ> ns) = \<zero>
[PROOF STEP]
using hensel_seq_comp_f
[PROOF STATE]
proof (prove)
using this:
res_lim ((\<bullet>) f \<circ> ns) = \<zero>

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain \<alpha> where alpha_def: "\<alpha> = res_lim ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha>. \<alpha> = res_lim ns \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<alpha> = res_lim ns

goal (1 subgoal):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have F1: "(f\<bullet>\<alpha>)= \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> \<alpha> = \<zero>
[PROOF STEP]
using F0 alpha_def alt_seq_limit
      ns_cauchy polynomial_is_Zp_continuous res_lim_pushforward
      res_lim_pushforward'
[PROOF STATE]
proof (prove)
using this:
res_lim ((\<bullet>) f \<circ> ns) = \<zero>
\<alpha> = res_lim ns
is_Zp_cauchy ?s \<Longrightarrow> res_lim (alt_seq ?s) = res_lim ?s
is_Zp_cauchy ns
?f \<in> carrier (UP Zp) \<Longrightarrow> is_Zp_continuous ((\<bullet>) ?f)
\<lbrakk>is_Zp_continuous ?f; is_Zp_cauchy ?s; ?t = alt_seq ?s\<rbrakk> \<Longrightarrow> res_lim (?f \<circ> ?t) = ?f (res_lim ?t)
\<lbrakk>is_Zp_continuous ?f; is_Zp_cauchy ?s; ?t = alt_seq ?s\<rbrakk> \<Longrightarrow> res_lim (?f \<circ> ?s) = res_lim (?f \<circ> ?t)

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have F2: "val_Zp (a \<ominus> \<alpha>) > val_Zp (f'\<bullet>a) \<and>  val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f\<bullet>a) (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have 0: "Zp_converges_to ns \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Zp_converges_to ns \<alpha>
[PROOF STEP]
by (simp add: alpha_def is_Zp_cauchy_imp_has_limit ns_cauchy)
[PROOF STATE]
proof (state)
this:
Zp_converges_to ns \<alpha>

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have "val_Zp (a \<ominus> \<alpha>) < \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) < \<infinity>
[PROOF STEP]
using "0" F1 R.r_right_minus_eq Zp_converges_to_def Zp_def hensel.fa_nonzero hensel_axioms local.a_closed val_Zp_def
[PROOF STATE]
proof (prove)
using this:
Zp_converges_to ns \<alpha>
f \<bullet> \<alpha> = \<zero>
\<lbrakk>?a \<in> carrier Zp; ?b \<in> carrier Zp\<rbrakk> \<Longrightarrow> (?a \<ominus> ?b = \<zero>) = (?a = ?b)
Zp_converges_to ?s ?a = ((?a \<in> carrier Zp \<and> ?s \<in> carrier Zp\<^bsup>\<omega>\<^esup>) \<and> (\<forall>n. \<exists>k. \<forall>m>k. eint n < val_Zp (?s m \<ominus> ?a)))
Zp \<equiv> padic_int p
hensel ?p ?f ?a \<Longrightarrow> UP_cring.to_fun (padic_int ?p) ?f ?a \<noteq> \<zero>\<^bsub>padic_int ?p\<^esub>
hensel p f a
a \<in> carrier Zp
val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))

goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) < \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> \<alpha>) < \<infinity>

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
hence "1 + max (eint 2 + val_Zp (f'\<bullet>a)) (val_Zp (\<alpha> \<ominus> a)) < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
val_Zp (a \<ominus> \<alpha>) < \<infinity>

goal (1 subgoal):
 1. 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < \<infinity>
[PROOF STEP]
by (metis "0" R.minus_closed Zp_converges_to_def eint.distinct(2) eint_ord_simps(4)
          f'a_not_infinite infinity_ne_i1 local.a_closed max_def minus_a_inv
          sum_infinity_imp_summand_infinity val_Zp_of_minus)
[PROOF STATE]
proof (state)
this:
1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < \<infinity>

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < \<infinity>
[PROOF STEP]
obtain l where l_def: "eint l = 1 + max (eint 2 + val_Zp (f'\<bullet>a)) (val_Zp (\<alpha> \<ominus> a))"
[PROOF STATE]
proof (prove)
using this:
1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < \<infinity>

goal (1 subgoal):
 1. (\<And>l. eint l = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eint l = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint l = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
[PROOF STEP]
obtain N where N_def: "(\<forall>m>N. 1 + max (2 + val_Zp (f'\<bullet>a)) (val_Zp (\<alpha> \<ominus> a)) < val_Zp_dist (ns m) \<alpha>)"
[PROOF STATE]
proof (prove)
using this:
eint l = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))

goal (1 subgoal):
 1. (\<And>N. \<forall>m>N. 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < val_Zp_dist (ns m) \<alpha> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 0 l_def Zp_converges_to_def[of ns \<alpha>]
[PROOF STATE]
proof (prove)
using this:
eint l = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
Zp_converges_to ns \<alpha>
eint l = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
Zp_converges_to ns \<alpha> = ((\<alpha> \<in> carrier Zp \<and> ns \<in> carrier Zp\<^bsup>\<omega>\<^esup>) \<and> (\<forall>n. \<exists>k. \<forall>m>k. eint n < val_Zp (ns m \<ominus> \<alpha>)))

goal (1 subgoal):
 1. (\<And>N. \<forall>m>N. 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < val_Zp_dist (ns m) \<alpha> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding val_Zp_dist_def
[PROOF STATE]
proof (prove)
using this:
eint l = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
Zp_converges_to ns \<alpha>
eint l = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
Zp_converges_to ns \<alpha> = ((\<alpha> \<in> carrier Zp \<and> ns \<in> carrier Zp\<^bsup>\<omega>\<^esup>) \<and> (\<forall>n. \<exists>k. \<forall>m>k. eint n < val_Zp (ns m \<ominus> \<alpha>)))

goal (1 subgoal):
 1. (\<And>N. \<forall>m>N. 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < val_Zp (ns m \<ominus> \<alpha>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>m>N. 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < val_Zp_dist (ns m) \<alpha>

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
obtain N' where N'_def: "\<forall>n>N'. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f\<bullet>a) (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N'. \<forall>n>N'. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pre_hensel(2)
[PROOF STATE]
proof (prove)
using this:
\<exists>N. \<forall>n>N. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

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

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
obtain K where K_def: "K = Suc (max N N')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>K. K = Suc (max N N') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
K = Suc (max N N')

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
K = Suc (max N N')
[PROOF STEP]
have F21: "(1+ (max (2 + val_Zp (f'\<bullet>a)) (val_Zp (\<alpha> \<ominus> a)))) < val_Zp_dist (ns K) \<alpha>"
[PROOF STATE]
proof (prove)
using this:
K = Suc (max N N')

goal (1 subgoal):
 1. 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < val_Zp_dist (ns K) \<alpha>
[PROOF STEP]
by (metis N_def lessI linorder_not_less max_def order_trans)
[PROOF STATE]
proof (state)
this:
1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < val_Zp_dist (ns K) \<alpha>

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have F22: "a \<noteq> ns K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> ns K
[PROOF STEP]
by (smt False K_def N'_def Zp_def cring_def eint.distinct(2) hensel_factor_id lessI
          less_le_trans linorder_not_less max_def mult_comm mult_zero_l newton_seq_closed
          order_less_le padic_int_is_cring padic_integers.prime padic_integers_axioms ring.r_right_minus_eq
          val_Zp_def)
[PROOF STATE]
proof (state)
this:
a \<noteq> ns K

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

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

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
using pre_hensel F1 False
[PROOF STATE]
proof (prove)
using this:
ns K = \<alpha>
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)
f \<bullet> \<alpha> = \<zero>
\<nexists>k. f \<bullet> ns k = \<zero>

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

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

goal (1 subgoal):
 1. ns K \<noteq> \<alpha> \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
assume "ns K \<noteq> \<alpha>"
[PROOF STATE]
proof (state)
this:
ns K \<noteq> \<alpha>

goal (1 subgoal):
 1. ns K \<noteq> \<alpha> \<Longrightarrow> val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have P0: " (a \<ominus> \<alpha>) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<ominus> \<alpha> \<in> nonzero Zp
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) F1 not_eq_diff_nonzero
              \<open>Zp_converges_to ns \<alpha>\<close> a_closed Zp_converges_to_def fa_nonzero)
[PROOF STATE]
proof (state)
this:
a \<ominus> \<alpha> \<in> nonzero Zp

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have P1: "(\<alpha> \<ominus> (ns K)) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<ominus> ns K \<in> nonzero Zp
[PROOF STEP]
using False not_eq_diff_nonzero \<open>Zp_converges_to ns \<alpha>\<close>
            Zp_converges_to_def newton_seq_closed
[PROOF STATE]
proof (prove)
using this:
ns K \<noteq> \<alpha>
\<lbrakk>?a \<noteq> ?b; ?a \<in> carrier Zp; ?b \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?a \<ominus> ?b \<in> nonzero Zp
Zp_converges_to ns \<alpha>
Zp_converges_to ?s ?a = ((?a \<in> carrier Zp \<and> ?s \<in> carrier Zp\<^bsup>\<omega>\<^esup>) \<and> (\<forall>n. \<exists>k. \<forall>m>k. eint n < val_Zp (?s m \<ominus> ?a)))
ns ?m \<in> carrier Zp

goal (1 subgoal):
 1. \<alpha> \<ominus> ns K \<in> nonzero Zp
[PROOF STEP]
by (metis (mono_tags, opaque_lifting))
[PROOF STATE]
proof (state)
this:
\<alpha> \<ominus> ns K \<in> nonzero Zp

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have P2: "a \<ominus> (ns K) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<ominus> ns K \<in> nonzero Zp
[PROOF STEP]
using F22 not_eq_diff_nonzero
                a_closed newton_seq_closed
[PROOF STATE]
proof (prove)
using this:
a \<noteq> ns K
\<lbrakk>?a \<noteq> ?b; ?a \<in> carrier Zp; ?b \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?a \<ominus> ?b \<in> nonzero Zp
a \<in> carrier Zp
ns ?m \<in> carrier Zp

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

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have P3: "(a \<ominus> \<alpha>) = a \<ominus> (ns K) \<oplus> ((ns K) \<ominus> \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<ominus> \<alpha> = a \<ominus> ns K \<oplus> (ns K \<ominus> \<alpha>)
[PROOF STEP]
by (metis R.plus_diff_simp \<open>Zp_converges_to ns \<alpha>\<close> add_comm Zp_converges_to_def local.a_closed newton_seq_closed)
[PROOF STATE]
proof (state)
this:
a \<ominus> \<alpha> = a \<ominus> ns K \<oplus> (ns K \<ominus> \<alpha>)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have P4: "val_Zp (a \<ominus> \<alpha>) \<ge> min (val_Zp (a \<ominus> (ns K))) (val_Zp ((ns K) \<ominus> \<alpha>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (val_Zp (a \<ominus> ns K)) (val_Zp (ns K \<ominus> \<alpha>)) \<le> val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
using "0" P3 Zp_converges_to_def newton_seq_closed val_Zp_ultrametric
[PROOF STATE]
proof (prove)
using this:
Zp_converges_to ns \<alpha>
a \<ominus> \<alpha> = a \<ominus> ns K \<oplus> (ns K \<ominus> \<alpha>)
Zp_converges_to ?s ?a = ((?a \<in> carrier Zp \<and> ?s \<in> carrier Zp\<^bsup>\<omega>\<^esup>) \<and> (\<forall>n. \<exists>k. \<forall>m>k. eint n < val_Zp (?s m \<ominus> ?a)))
ns ?m \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> min (val_Zp ?x) (val_Zp ?y) \<le> val_Zp (?x \<oplus> ?y)

goal (1 subgoal):
 1. min (val_Zp (a \<ominus> ns K)) (val_Zp (ns K \<ominus> \<alpha>)) \<le> val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
min (val_Zp (a \<ominus> ns K)) (val_Zp (ns K \<ominus> \<alpha>)) \<le> val_Zp (a \<ominus> \<alpha>)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have P5: "val_Zp (a \<ominus> (ns K)) >  val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns K)
[PROOF STEP]
using pre_hensel(1)[of "K"]
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns K)

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

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have "1 + max (eint 2 + val_Zp (f'\<bullet>a)) (val_Zp (\<alpha> \<ominus> a)) > val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
[PROOF STEP]
have "1 + max (eint 2 + val_Zp (f'\<bullet>a)) (val_Zp (\<alpha> \<ominus> a)) > (eint 2 + val_Zp (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 + val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eint 2 + val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
[PROOF STEP]
obtain ii :: int where
              f1: "eint ii = 1 + max (eint 2 + val_Zp (f'\<bullet>a)) (val_Zp (\<alpha> \<ominus> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ii. eint ii = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson l_def)
[PROOF STATE]
proof (state)
this:
eint ii = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))

goal (1 subgoal):
 1. eint 2 + val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint ii = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
[PROOF STEP]
have "1 + (eint 2 + val_Zp (f'\<bullet>a)) \<le> eint ii"
[PROOF STATE]
proof (prove)
using this:
eint ii = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))

goal (1 subgoal):
 1. 1 + (eint 2 + val_Zp (f' \<bullet> a)) \<le> eint ii
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 + (eint 2 + val_Zp (f' \<bullet> a)) \<le> eint ii

goal (1 subgoal):
 1. eint 2 + val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 + (eint 2 + val_Zp (f' \<bullet> a)) \<le> eint ii
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 + (eint 2 + val_Zp (f' \<bullet> a)) \<le> eint ii

goal (1 subgoal):
 1. eint 2 + val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
1 + (eint 2 + val_Zp (f' \<bullet> a)) \<le> eint ii
eint ii = 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))

goal (1 subgoal):
 1. eint 2 + val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
[PROOF STEP]
by (metis Groups.add_ac(2) iless_Suc_eq linorder_not_less)
[PROOF STATE]
proof (state)
this:
eint 2 + val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint 2 + val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eint 2 + val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
[PROOF STEP]
by (smt Groups.add_ac(2) eint_pow_int_is_pos f'a_not_infinite ge_plus_pos_imp_gt order_less_le)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
hence P6: "val_Zp ((ns K) \<ominus> \<alpha>) >  val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (ns K \<ominus> \<alpha>)
[PROOF STEP]
using F21
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < val_Zp_dist (ns K) \<alpha>

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (ns K \<ominus> \<alpha>)
[PROOF STEP]
unfolding val_Zp_dist_def
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> a) < 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a))
1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < val_Zp (ns K \<ominus> \<alpha>)

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

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have P7: "val_Zp (a \<ominus> \<alpha>) >  val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
[PROOF STEP]
using P4 P5 P6 eint_min_ineq
[PROOF STATE]
proof (prove)
using this:
min (val_Zp (a \<ominus> ns K)) (val_Zp (ns K \<ominus> \<alpha>)) \<le> val_Zp (a \<ominus> \<alpha>)
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ns K)
val_Zp (f' \<bullet> a) < val_Zp (ns K \<ominus> \<alpha>)
\<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> \<alpha>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have P8:  "val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f\<bullet>a) (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have " 1 + max (2 + val_Zp (f'\<bullet>a)) (val_Zp_dist \<alpha> a) \<le> val_Zp_dist (ns K) \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp_dist \<alpha> a) \<le> val_Zp_dist (ns K) \<alpha>
[PROOF STEP]
using False F21
[PROOF STATE]
proof (prove)
using this:
ns K \<noteq> \<alpha>
1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp (\<alpha> \<ominus> a)) < val_Zp_dist (ns K) \<alpha>

goal (1 subgoal):
 1. 1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp_dist \<alpha> a) \<le> val_Zp_dist (ns K) \<alpha>
[PROOF STEP]
by (simp add: val_Zp_dist_def)
[PROOF STATE]
proof (state)
this:
1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp_dist \<alpha> a) \<le> val_Zp_dist (ns K) \<alpha>

goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp_dist \<alpha> a) \<le> val_Zp_dist (ns K) \<alpha>
[PROOF STEP]
have "val_Zp(\<alpha> \<ominus> (ns K)) >   max (2 + val_Zp (f'\<bullet>a)) (val_Zp_dist \<alpha> a)"
[PROOF STATE]
proof (prove)
using this:
1 + max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp_dist \<alpha> a) \<le> val_Zp_dist (ns K) \<alpha>

goal (1 subgoal):
 1. max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp_dist \<alpha> a) < val_Zp (\<alpha> \<ominus> ns K)
[PROOF STEP]
by (metis "0" Groups.add_ac(2) P1 Zp_converges_to_def eSuc_mono iless_Suc_eq l_def
                minus_a_inv newton_seq_closed nonzero_closed val_Zp_dist_def val_Zp_of_minus)
[PROOF STATE]
proof (state)
this:
max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp_dist \<alpha> a) < val_Zp (\<alpha> \<ominus> ns K)

goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp_dist \<alpha> a) < val_Zp (\<alpha> \<ominus> ns K)
[PROOF STEP]
have "val_Zp(\<alpha> \<ominus> (ns K)) > val_Zp (a \<ominus> \<alpha>) "
[PROOF STATE]
proof (prove)
using this:
max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp_dist \<alpha> a) < val_Zp (\<alpha> \<ominus> ns K)

goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) < val_Zp (\<alpha> \<ominus> ns K)
[PROOF STEP]
using \<open>Zp_converges_to ns \<alpha>\<close> Zp_converges_to_def val_Zp_dist_def val_Zp_dist_sym
[PROOF STATE]
proof (prove)
using this:
max (eint 2 + val_Zp (f' \<bullet> a)) (val_Zp_dist \<alpha> a) < val_Zp (\<alpha> \<ominus> ns K)
Zp_converges_to ns \<alpha>
Zp_converges_to ?s ?a = ((?a \<in> carrier Zp \<and> ?s \<in> carrier Zp\<^bsup>\<omega>\<^esup>) \<and> (\<forall>n. \<exists>k. \<forall>m>k. eint n < val_Zp (?s m \<ominus> ?a)))
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

goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) < val_Zp (\<alpha> \<ominus> ns K)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> \<alpha>) < val_Zp (\<alpha> \<ominus> ns K)

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

goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) = val_Zp (a \<ominus> ns K)
[PROOF STEP]
using P0 P1 Zp_def val_Zp_ultrametric_eq[of "\<alpha> \<ominus> ns K" "a \<ominus> \<alpha>"] 0 R.plus_diff_simp
              Zp_converges_to_def local.a_closed newton_seq_closed nonzero_closed
[PROOF STATE]
proof (prove)
using this:
val_Zp (a \<ominus> \<alpha>) < val_Zp (\<alpha> \<ominus> ns K)
a \<ominus> \<alpha> \<in> nonzero Zp
\<alpha> \<ominus> ns K \<in> nonzero Zp
Zp \<equiv> padic_int p
\<lbrakk>\<alpha> \<ominus> ns K \<in> carrier Zp; a \<ominus> \<alpha> \<in> carrier Zp; val_Zp (a \<ominus> \<alpha>) < val_Zp (\<alpha> \<ominus> ns K)\<rbrakk> \<Longrightarrow> val_Zp (\<alpha> \<ominus> ns K \<oplus> (a \<ominus> \<alpha>)) = val_Zp (a \<ominus> \<alpha>)
Zp_converges_to ns \<alpha>
\<lbrakk>?a \<in> carrier Zp; ?b \<in> carrier Zp; ?c \<in> carrier Zp; ?X = ?a \<ominus> ?b; ?Y = ?c \<ominus> ?a\<rbrakk> \<Longrightarrow> ?X \<oplus> ?Y = ?c \<ominus> ?b
Zp_converges_to ?s ?a = ((?a \<in> carrier Zp \<and> ?s \<in> carrier Zp\<^bsup>\<omega>\<^esup>) \<and> (\<forall>n. \<exists>k. \<forall>m>k. eint n < val_Zp (?s m \<ominus> ?a)))
a \<in> carrier Zp
ns ?m \<in> carrier Zp
?a \<in> nonzero Zp \<Longrightarrow> ?a \<in> carrier Zp

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

goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
have P81: "val_Zp (a \<ominus> ns K) = val_Zp (local.divide (f\<bullet>a) (f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (a \<ominus> ns K) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
using K_def N'_def
[PROOF STATE]
proof (prove)
using this:
K = Suc (max N N')
\<forall>n>N'. val_Zp (a \<ominus> ns n) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (a \<ominus> ns K) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
by (metis (no_types, lifting) lessI linorder_not_less max_def order_less_le order_trans)
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> ns K) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (a \<ominus> ns K) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp (a \<ominus> ns K) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
by (simp add: P80)
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> \<alpha>) = 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> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))

goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
[PROOF STEP]
using P7
[PROOF STATE]
proof (prove)
using this:
val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>)

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have F3: "val_Zp (f' \<bullet> \<alpha>) = val_Zp (f'\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)
[PROOF STEP]
have F31: " (f' \<bullet> \<alpha>) = res_lim ((to_fun f') \<circ> ns)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> \<alpha> = res_lim ((\<bullet>) f' \<circ> ns)
[PROOF STEP]
using alpha_def alt_seq_limit ns_cauchy polynomial_is_Zp_continuous res_lim_pushforward
          res_lim_pushforward' f'_closed
[PROOF STATE]
proof (prove)
using this:
\<alpha> = res_lim ns
is_Zp_cauchy ?s \<Longrightarrow> res_lim (alt_seq ?s) = res_lim ?s
is_Zp_cauchy ns
?f \<in> carrier (UP Zp) \<Longrightarrow> is_Zp_continuous ((\<bullet>) ?f)
\<lbrakk>is_Zp_continuous ?f; is_Zp_cauchy ?s; ?t = alt_seq ?s\<rbrakk> \<Longrightarrow> res_lim (?f \<circ> ?t) = ?f (res_lim ?t)
\<lbrakk>is_Zp_continuous ?f; is_Zp_cauchy ?s; ?t = alt_seq ?s\<rbrakk> \<Longrightarrow> res_lim (?f \<circ> ?s) = res_lim (?f \<circ> ?t)
f' \<in> carrier (UP Zp)

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

goal (1 subgoal):
 1. val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)
[PROOF STEP]
obtain N where N_def: "val_Zp (f'\<bullet>\<alpha> \<ominus> f'\<bullet>(ns N)) > val_Zp ((f'\<bullet>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. val_Zp (f' \<bullet> a) < val_Zp (f' \<bullet> \<alpha> \<ominus> f' \<bullet> ns N) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (smt F2 False R.minus_closed Suc_ile_eq Zp_def alpha_def f'_closed f'a_nonzero
          local.a_closed minus_a_inv newton_seq.simps(1) newton_seq_is_Zp_cauchy_0 order_trans
          padic_integers.poly_diff_val padic_integers_axioms res_lim_in_Zp val_Zp_def val_Zp_of_minus)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> a) < val_Zp (f' \<bullet> \<alpha> \<ominus> f' \<bullet> ns N)

goal (1 subgoal):
 1. val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)
[PROOF STEP]
by (metis False N_def alpha_def equal_val_Zp f'_closed newton_seq_closed newton_seq_is_Zp_cauchy_0 newton_seq_fact1 res_lim_in_Zp to_fun_closed)
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. f \<bullet> ns k = \<zero>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using F1 F2 F3 that alpha_def ns_cauchy res_lim_in_Zp
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<alpha> = \<zero>
val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> \<alpha>) \<and> val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a))
val_Zp (f' \<bullet> \<alpha>) = val_Zp (f' \<bullet> a)
\<lbrakk>f \<bullet> ?\<alpha>2 = \<zero>; ?\<alpha>2 \<in> carrier Zp; val_Zp (f' \<bullet> a) < val_Zp (a \<ominus> ?\<alpha>2); val_Zp (a \<ominus> ?\<alpha>2) = val_Zp (local.divide (f \<bullet> a) (f' \<bullet> a)); val_Zp (f' \<bullet> ?\<alpha>2) = val_Zp (f' \<bullet> a)\<rbrakk> \<Longrightarrow> thesis
\<alpha> = res_lim ns
is_Zp_cauchy ns
is_Zp_cauchy ?s \<Longrightarrow> res_lim ?s \<in> carrier Zp

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hensels_lemma:
  assumes "f \<in> carrier Zp_x"
  assumes "a \<in> carrier Zp"
  assumes "(pderiv f)\<bullet>a \<noteq> \<zero>"
  assumes "f\<bullet>a \<noteq>\<zero>"
  assumes "val_Zp (f\<bullet>a) > 2* val_Zp ((pderiv f)\<bullet>a)"
  obtains \<alpha> where
       "f\<bullet>\<alpha> = \<zero>" and "\<alpha> \<in> carrier Zp"
       "val_Zp (a \<ominus> \<alpha>) > val_Zp ((pderiv f)\<bullet>a)"
       "val_Zp (a \<ominus> \<alpha>) = val_Zp (divide (f\<bullet>a) ((pderiv f)\<bullet>a))"
       "val_Zp ((pderiv f)\<bullet>\<alpha>) = val_Zp ((pderiv f)\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (pderiv f \<bullet> a)); val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (pderiv f \<bullet> a)); val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "hensel p f a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hensel p f a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> carrier (UP Zp)
a \<in> carrier Zp
pderiv f \<bullet> a \<noteq> \<zero>
f \<bullet> a \<noteq> \<zero>
eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. hensel p f a
[PROOF STEP]
by (simp add: Zp_def hensel.intro hensel_axioms.intro padic_integers_axioms)
[PROOF STATE]
proof (state)
this:
hensel p f a

goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>); val_Zp (a \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> a) (pderiv f \<bullet> a)); val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hensel p f a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hensel p f a

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using hensel.full_hensels_lemma  Zp_def that
[PROOF STATE]
proof (prove)
using this:
hensel p f a
\<lbrakk>hensel ?p ?f ?a; \<And>\<alpha>. \<lbrakk>UP_cring.to_fun (padic_int ?p) ?f \<alpha> = \<zero>\<^bsub>padic_int ?p\<^esub>; \<alpha> \<in> carrier (padic_int ?p); padic_integers.val_Zp ?p (UP_cring.to_fun (padic_int ?p) (UP_cring.pderiv (padic_int ?p) ?f) ?a) < padic_integers.val_Zp ?p (?a \<ominus>\<^bsub>padic_int ?p\<^esub> \<alpha>); padic_integers.val_Zp ?p (?a \<ominus>\<^bsub>padic_int ?p\<^esub> \<alpha>) = padic_integers.val_Zp ?p (padic_integers.divide ?p (UP_cring.to_fun (padic_int ?p) ?f ?a) (UP_cring.to_fun (padic_int ?p) (UP_cring.pderiv (padic_int ?p) ?f) ?a)); padic_integers.val_Zp ?p (UP_cring.to_fun (padic_int ?p) (UP_cring.pderiv (padic_int ?p) ?f) \<alpha>) = padic_integers.val_Zp ?p (UP_cring.to_fun (padic_int ?p) (UP_cring.pderiv (padic_int ?p) ?f) ?a)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
Zp \<equiv> padic_int p
\<lbrakk>f \<bullet> ?\<alpha>2 = \<zero>; ?\<alpha>2 \<in> carrier Zp; val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> ?\<alpha>2); val_Zp (a \<ominus> ?\<alpha>2) = val_Zp (local.divide (f \<bullet> a) (pderiv f \<bullet> a)); val_Zp (pderiv f \<bullet> ?\<alpha>2) = val_Zp (pderiv f \<bullet> a)\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hensels_lemma_unique_root:
  assumes "f \<in> carrier Zp_x"
  assumes "a \<in> carrier Zp"
  assumes "(pderiv f)\<bullet>a \<noteq> \<zero>"
  assumes "f\<bullet>a \<noteq>\<zero>"
  assumes "(val_Zp (f\<bullet>a) > 2* val_Zp ((pderiv f)\<bullet>a))"
  assumes "f\<bullet>\<alpha> = \<zero>"
  assumes "\<alpha> \<in> carrier Zp"
  assumes "val_Zp (a \<ominus> \<alpha>) > val_Zp ((pderiv f)\<bullet>a)"
  assumes "f\<bullet>\<beta> = \<zero>"
  assumes "\<beta> \<in> carrier Zp"
  assumes "val_Zp (a \<ominus> \<beta>) > val_Zp ((pderiv f)\<bullet>a)"
  assumes "val_Zp ((pderiv f)\<bullet>\<alpha>) = val_Zp ((pderiv f)\<bullet>a)"
  shows "\<alpha> = \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
have "\<alpha> \<noteq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<noteq> a
[PROOF STEP]
using assms(4) assms(6)
[PROOF STATE]
proof (prove)
using this:
f \<bullet> a \<noteq> \<zero>
f \<bullet> \<alpha> = \<zero>

goal (1 subgoal):
 1. \<alpha> \<noteq> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> \<noteq> a

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
have "\<beta> \<noteq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<beta> \<noteq> a
[PROOF STEP]
using assms(4) assms(9)
[PROOF STATE]
proof (prove)
using this:
f \<bullet> a \<noteq> \<zero>
f \<bullet> \<beta> = \<zero>

goal (1 subgoal):
 1. \<beta> \<noteq> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<beta> \<noteq> a

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
have 0: "val_Zp (\<beta> \<ominus> \<alpha>) >  val_Zp ((pderiv f)\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) < val_Zp (\<beta> \<ominus> \<alpha>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) < val_Zp (\<beta> \<ominus> \<alpha>)
[PROOF STEP]
have "\<beta> \<ominus> \<alpha> = \<ominus> ((a \<ominus> \<beta>) \<ominus> (a \<ominus> \<alpha>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<beta> \<ominus> \<alpha> = \<ominus> (a \<ominus> \<beta> \<ominus> (a \<ominus> \<alpha>))
[PROOF STEP]
by (metis R.minus_eq R.plus_diff_simp assms(10) assms(2) assms(7) minus_a_inv)
[PROOF STATE]
proof (state)
this:
\<beta> \<ominus> \<alpha> = \<ominus> (a \<ominus> \<beta> \<ominus> (a \<ominus> \<alpha>))

goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) < val_Zp (\<beta> \<ominus> \<alpha>)
[PROOF STEP]
hence "val_Zp (\<beta> \<ominus> \<alpha>) = val_Zp ((a \<ominus> \<beta>) \<ominus> (a \<ominus> \<alpha>))"
[PROOF STATE]
proof (prove)
using this:
\<beta> \<ominus> \<alpha> = \<ominus> (a \<ominus> \<beta> \<ominus> (a \<ominus> \<alpha>))

goal (1 subgoal):
 1. val_Zp (\<beta> \<ominus> \<alpha>) = val_Zp (a \<ominus> \<beta> \<ominus> (a \<ominus> \<alpha>))
[PROOF STEP]
using R.minus_closed assms(10) assms(2) assms(7) val_Zp_of_minus
[PROOF STATE]
proof (prove)
using this:
\<beta> \<ominus> \<alpha> = \<ominus> (a \<ominus> \<beta> \<ominus> (a \<ominus> \<alpha>))
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<ominus> ?y \<in> carrier Zp
\<beta> \<in> carrier Zp
a \<in> carrier Zp
\<alpha> \<in> carrier Zp
?a \<in> carrier Zp \<Longrightarrow> val_Zp ?a = val_Zp (\<ominus> ?a)

goal (1 subgoal):
 1. val_Zp (\<beta> \<ominus> \<alpha>) = val_Zp (a \<ominus> \<beta> \<ominus> (a \<ominus> \<alpha>))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
val_Zp (\<beta> \<ominus> \<alpha>) = val_Zp (a \<ominus> \<beta> \<ominus> (a \<ominus> \<alpha>))

goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) < val_Zp (\<beta> \<ominus> \<alpha>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp (\<beta> \<ominus> \<alpha>) = val_Zp (a \<ominus> \<beta> \<ominus> (a \<ominus> \<alpha>))

goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) < val_Zp (\<beta> \<ominus> \<alpha>)
[PROOF STEP]
using val_Zp_ultrametric_diff[of "a \<ominus> \<beta>" "a \<ominus> \<alpha>"]
[PROOF STATE]
proof (prove)
using this:
val_Zp (\<beta> \<ominus> \<alpha>) = val_Zp (a \<ominus> \<beta> \<ominus> (a \<ominus> \<alpha>))
\<lbrakk>a \<ominus> \<beta> \<in> carrier Zp; a \<ominus> \<alpha> \<in> carrier Zp\<rbrakk> \<Longrightarrow> min (val_Zp (a \<ominus> \<beta>)) (val_Zp (a \<ominus> \<alpha>)) \<le> val_Zp (a \<ominus> \<beta> \<ominus> (a \<ominus> \<alpha>))

goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) < val_Zp (\<beta> \<ominus> \<alpha>)
[PROOF STEP]
by (smt R.minus_closed assms(10) assms(11) assms(2) assms(7) assms(8) min.absorb2 min_less_iff_conj)
[PROOF STATE]
proof (state)
this:
val_Zp (pderiv f \<bullet> a) < val_Zp (\<beta> \<ominus> \<alpha>)

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

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
obtain h where h_def: "h = \<beta> \<ominus> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. h = \<beta> \<ominus> \<alpha> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
h = \<beta> \<ominus> \<alpha>

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h = \<beta> \<ominus> \<alpha>
[PROOF STEP]
have h_fact: "h \<in> carrier Zp \<and> \<beta> = \<alpha> \<oplus> h"
[PROOF STATE]
proof (prove)
using this:
h = \<beta> \<ominus> \<alpha>

goal (1 subgoal):
 1. h \<in> carrier Zp \<and> \<beta> = \<alpha> \<oplus> h
[PROOF STEP]
by (metis R.l_neg R.minus_closed R.minus_eq R.r_zero add_assoc add_comm assms(10) assms(7))
[PROOF STATE]
proof (state)
this:
h \<in> carrier Zp \<and> \<beta> = \<alpha> \<oplus> h

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h \<in> carrier Zp \<and> \<beta> = \<alpha> \<oplus> h
[PROOF STEP]
have 1: "f\<bullet>(\<alpha> \<oplus> h) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
h \<in> carrier Zp \<and> \<beta> = \<alpha> \<oplus> h

goal (1 subgoal):
 1. f \<bullet> (\<alpha> \<oplus> h) = \<zero>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h \<in> carrier Zp \<and> \<beta> = \<alpha> \<oplus> h
f \<in> carrier (UP Zp)
a \<in> carrier Zp
pderiv f \<bullet> a \<noteq> \<zero>
f \<bullet> a \<noteq> \<zero>
eint 2 * val_Zp (pderiv f \<bullet> a) < val_Zp (f \<bullet> a)
f \<bullet> \<alpha> = \<zero>
\<alpha> \<in> carrier Zp
val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<alpha>)
f \<bullet> \<beta> = \<zero>
\<beta> \<in> carrier Zp
val_Zp (pderiv f \<bullet> a) < val_Zp (a \<ominus> \<beta>)
val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> a)

goal (1 subgoal):
 1. f \<bullet> (\<alpha> \<oplus> h) = \<zero>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<bullet> (\<alpha> \<oplus> h) = \<zero>

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
obtain c where c_def: "c \<in> carrier Zp \<and> f\<bullet>(\<alpha> \<oplus> h) = (f \<bullet> \<alpha>) \<oplus> (deriv f \<alpha>)\<otimes>h \<oplus> c \<otimes>(h[^](2::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. c \<in> carrier Zp \<and> f \<bullet> (\<alpha> \<oplus> h) = f \<bullet> \<alpha> \<oplus> deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using taylor_deg_1_eval'[of  f \<alpha> h _ "f \<bullet> \<alpha>" "deriv f \<alpha>" ]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f \<in> carrier (UP Zp); \<alpha> \<in> carrier Zp; h \<in> carrier Zp; ?c = shift 2 (taylor \<alpha> f) \<bullet> h; f \<bullet> \<alpha> = f \<bullet> \<alpha>; deriv f \<alpha> = deriv f \<alpha>\<rbrakk> \<Longrightarrow> f \<bullet> (\<alpha> \<oplus> h) = f \<bullet> \<alpha> \<oplus> deriv f \<alpha> \<otimes> h \<oplus> ?c \<otimes> h [^] 2

goal (1 subgoal):
 1. (\<And>c. c \<in> carrier Zp \<and> f \<bullet> (\<alpha> \<oplus> h) = f \<bullet> \<alpha> \<oplus> deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson taylor_closed assms(1) assms(7) to_fun_closed h_fact shift_closed)
[PROOF STATE]
proof (state)
this:
c \<in> carrier Zp \<and> f \<bullet> (\<alpha> \<oplus> h) = f \<bullet> \<alpha> \<oplus> deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<in> carrier Zp \<and> f \<bullet> (\<alpha> \<oplus> h) = f \<bullet> \<alpha> \<oplus> deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2
[PROOF STEP]
have  "(f \<bullet> \<alpha>) \<oplus> (deriv f \<alpha>)\<otimes>h \<oplus> c \<otimes>(h[^](2::nat)) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
c \<in> carrier Zp \<and> f \<bullet> (\<alpha> \<oplus> h) = f \<bullet> \<alpha> \<oplus> deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2

goal (1 subgoal):
 1. f \<bullet> \<alpha> \<oplus> deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>
[PROOF STEP]
by (simp add: "1")
[PROOF STATE]
proof (state)
this:
f \<bullet> \<alpha> \<oplus> deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<bullet> \<alpha> \<oplus> deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>
[PROOF STEP]
have 2:  "(deriv f \<alpha>)\<otimes>h \<oplus> c \<otimes>(h[^](2::nat)) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<alpha> \<oplus> deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>

goal (1 subgoal):
 1. deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>
[PROOF STEP]
by (simp add: assms(1) assms(6) assms(7) deriv_closed h_fact)
[PROOF STATE]
proof (state)
this:
deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
have 3: "((deriv f \<alpha>) \<oplus> c \<otimes>h)\<otimes>h = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
have "((deriv f \<alpha>) \<oplus> c \<otimes>h)\<otimes>h = ((deriv f \<alpha>)\<otimes>h \<oplus> (c \<otimes>h)\<otimes>h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h \<otimes> h
[PROOF STEP]
by (simp add: R.r_distr UP_cring.deriv_closed Zp_x_is_UP_cring assms(1) assms(7) c_def h_fact mult_comm)
[PROOF STATE]
proof (state)
this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h \<otimes> h

goal (1 subgoal):
 1. (deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h \<otimes> h
[PROOF STEP]
have "((deriv f \<alpha>) \<oplus> c \<otimes>h)\<otimes>h = (deriv f \<alpha>)\<otimes>h \<oplus> (c \<otimes>(h\<otimes>h))"
[PROOF STATE]
proof (prove)
using this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h \<otimes> h

goal (1 subgoal):
 1. (deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> (h \<otimes> h)
[PROOF STEP]
by (simp add: mult_assoc)
[PROOF STATE]
proof (state)
this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> (h \<otimes> h)

goal (1 subgoal):
 1. (deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> (h \<otimes> h)
[PROOF STEP]
have "((deriv f \<alpha>) \<oplus> c \<otimes>h)\<otimes>h = (deriv f \<alpha>)\<otimes>h \<oplus> (c \<otimes>(h[^](2::nat)))"
[PROOF STATE]
proof (prove)
using this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> (h \<otimes> h)

goal (1 subgoal):
 1. (deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2
[PROOF STEP]
using nat_pow_def[of Zp h "2"]
[PROOF STATE]
proof (prove)
using this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> (h \<otimes> h)
h [^] 2 = rec_nat \<one> (\<lambda>u b. b \<otimes> h) 2

goal (1 subgoal):
 1. (deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2
[PROOF STEP]
by (simp add: h_fact)
[PROOF STATE]
proof (state)
this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2

goal (1 subgoal):
 1. (deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2

goal (1 subgoal):
 1. (deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2
deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>

goal (1 subgoal):
 1. (deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = \<zero>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = \<zero>

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
have "h = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = \<zero>
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
assume "h \<noteq> \<zero>"
[PROOF STATE]
proof (state)
this:
h \<noteq> \<zero>

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h \<noteq> \<zero>
[PROOF STEP]
have "(deriv f \<alpha>) \<oplus> c \<otimes>h = \<zero>"
[PROOF STATE]
proof (prove)
using this:
h \<noteq> \<zero>

goal (1 subgoal):
 1. deriv f \<alpha> \<oplus> c \<otimes> h = \<zero>
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
h \<noteq> \<zero>
deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2 = \<zero>
(deriv f \<alpha> \<oplus> c \<otimes> h) \<otimes> h = \<zero>

goal (1 subgoal):
 1. deriv f \<alpha> \<oplus> c \<otimes> h = \<zero>
[PROOF STEP]
by (meson R.m_closed assms(1) assms(7) c_def deriv_closed h_fact local.integral sum_closed)
[PROOF STATE]
proof (state)
this:
deriv f \<alpha> \<oplus> c \<otimes> h = \<zero>

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv f \<alpha> \<oplus> c \<otimes> h = \<zero>
[PROOF STEP]
have "(deriv f \<alpha>) = \<ominus> c \<otimes>h"
[PROOF STATE]
proof (prove)
using this:
deriv f \<alpha> \<oplus> c \<otimes> h = \<zero>

goal (1 subgoal):
 1. deriv f \<alpha> = \<ominus> c \<otimes> h
[PROOF STEP]
by (simp add: R.l_minus R.sum_zero_eq_neg UP_cring.deriv_closed Zp_x_is_UP_cring assms(1) assms(7) c_def h_fact)
[PROOF STATE]
proof (state)
this:
deriv f \<alpha> = \<ominus> c \<otimes> h

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv f \<alpha> = \<ominus> c \<otimes> h
[PROOF STEP]
have "val_Zp (deriv f \<alpha>) = val_Zp (c \<otimes> h)"
[PROOF STATE]
proof (prove)
using this:
deriv f \<alpha> = \<ominus> c \<otimes> h

goal (1 subgoal):
 1. val_Zp (deriv f \<alpha>) = val_Zp (c \<otimes> h)
[PROOF STEP]
by (meson R.m_closed \<open>deriv f \<alpha> \<oplus> c \<otimes> h = \<zero>\<close> assms(1) assms(7) c_def deriv_closed h_fact val_Zp_not_equal_imp_notequal(3))
[PROOF STATE]
proof (state)
this:
val_Zp (deriv f \<alpha>) = val_Zp (c \<otimes> h)

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (deriv f \<alpha>) = val_Zp (c \<otimes> h)
[PROOF STEP]
have P: "val_Zp (deriv f \<alpha>) = val_Zp h + val_Zp c"
[PROOF STATE]
proof (prove)
using this:
val_Zp (deriv f \<alpha>) = val_Zp (c \<otimes> h)

goal (1 subgoal):
 1. val_Zp (deriv f \<alpha>) = val_Zp h + val_Zp c
[PROOF STEP]
using val_Zp_mult c_def h_fact
[PROOF STATE]
proof (prove)
using this:
val_Zp (deriv f \<alpha>) = val_Zp (c \<otimes> h)
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> val_Zp (?x \<otimes> ?y) = val_Zp ?x + val_Zp ?y
c \<in> carrier Zp \<and> f \<bullet> (\<alpha> \<oplus> h) = f \<bullet> \<alpha> \<oplus> deriv f \<alpha> \<otimes> h \<oplus> c \<otimes> h [^] 2
h \<in> carrier Zp \<and> \<beta> = \<alpha> \<oplus> h

goal (1 subgoal):
 1. val_Zp (deriv f \<alpha>) = val_Zp h + val_Zp c
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
val_Zp (deriv f \<alpha>) = val_Zp h + val_Zp c

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
hence "val_Zp (deriv f \<alpha>) \<ge> val_Zp h "
[PROOF STATE]
proof (prove)
using this:
val_Zp (deriv f \<alpha>) = val_Zp h + val_Zp c

goal (1 subgoal):
 1. val_Zp h \<le> val_Zp (deriv f \<alpha>)
[PROOF STEP]
using val_pos[of c]
[PROOF STATE]
proof (prove)
using this:
val_Zp (deriv f \<alpha>) = val_Zp h + val_Zp c
c \<in> carrier Zp \<Longrightarrow> 0 \<le> val_Zp c

goal (1 subgoal):
 1. val_Zp h \<le> val_Zp (deriv f \<alpha>)
[PROOF STEP]
by (simp add: c_def)
[PROOF STATE]
proof (state)
this:
val_Zp h \<le> val_Zp (deriv f \<alpha>)

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp h \<le> val_Zp (deriv f \<alpha>)
[PROOF STEP]
have "val_Zp (deriv f \<alpha>) \<ge> val_Zp (\<beta> \<ominus> \<alpha>) "
[PROOF STATE]
proof (prove)
using this:
val_Zp h \<le> val_Zp (deriv f \<alpha>)

goal (1 subgoal):
 1. val_Zp (\<beta> \<ominus> \<alpha>) \<le> val_Zp (deriv f \<alpha>)
[PROOF STEP]
using h_def
[PROOF STATE]
proof (prove)
using this:
val_Zp h \<le> val_Zp (deriv f \<alpha>)
h = \<beta> \<ominus> \<alpha>

goal (1 subgoal):
 1. val_Zp (\<beta> \<ominus> \<alpha>) \<le> val_Zp (deriv f \<alpha>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (\<beta> \<ominus> \<alpha>) \<le> val_Zp (deriv f \<alpha>)

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (\<beta> \<ominus> \<alpha>) \<le> val_Zp (deriv f \<alpha>)
[PROOF STEP]
have "val_Zp (deriv f \<alpha>) > val_Zp ((pderiv f)\<bullet>a)"
[PROOF STATE]
proof (prove)
using this:
val_Zp (\<beta> \<ominus> \<alpha>) \<le> val_Zp (deriv f \<alpha>)

goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) < val_Zp (deriv f \<alpha>)
[PROOF STEP]
using "0"
[PROOF STATE]
proof (prove)
using this:
val_Zp (\<beta> \<ominus> \<alpha>) \<le> val_Zp (deriv f \<alpha>)
val_Zp (pderiv f \<bullet> a) < val_Zp (\<beta> \<ominus> \<alpha>)

goal (1 subgoal):
 1. val_Zp (pderiv f \<bullet> a) < val_Zp (deriv f \<alpha>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp (pderiv f \<bullet> a) < val_Zp (deriv f \<alpha>)

goal (1 subgoal):
 1. h \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (pderiv f \<bullet> a) < val_Zp (deriv f \<alpha>)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
val_Zp (pderiv f \<bullet> a) < val_Zp (deriv f \<alpha>)

goal (1 subgoal):
 1. False
[PROOF STEP]
using pderiv_eval_deriv[of f \<alpha>]
[PROOF STATE]
proof (prove)
using this:
val_Zp (pderiv f \<bullet> a) < val_Zp (deriv f \<alpha>)
\<lbrakk>f \<in> carrier (UP Zp); \<alpha> \<in> carrier Zp\<rbrakk> \<Longrightarrow> deriv f \<alpha> = pderiv f \<bullet> \<alpha>

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(1) assms(12) assms(7)
[PROOF STATE]
proof (prove)
using this:
val_Zp (pderiv f \<bullet> a) < val_Zp (deriv f \<alpha>)
\<lbrakk>f \<in> carrier (UP Zp); \<alpha> \<in> carrier Zp\<rbrakk> \<Longrightarrow> deriv f \<alpha> = pderiv f \<bullet> \<alpha>
f \<in> carrier (UP Zp)
val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> a)
\<alpha> \<in> carrier Zp

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
h = \<zero>

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h = \<zero>
[PROOF STEP]
show "\<alpha> = \<beta>"
[PROOF STATE]
proof (prove)
using this:
h = \<zero>

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
using assms(10) assms(7) h_def
[PROOF STATE]
proof (prove)
using this:
h = \<zero>
\<beta> \<in> carrier Zp
\<alpha> \<in> carrier Zp
h = \<beta> \<ominus> \<alpha>

goal (1 subgoal):
 1. \<alpha> = \<beta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> = \<beta>

goal:
No subgoals!
[PROOF STEP]
qed