[STATEMENT]
lemma newton_seq_fact7:
 "(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.simps(2)[of n]  newton_seq_fact5[of n]
        newton_seq_closed[of "Suc n"]  newton_seq_closed[of n]
        R.ring_simprules
[PROOF STATE]
proof (prove)
using this:
ns (Suc n) = newton_step (ns n)
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
ns (Suc n) \<in> carrier Zp
ns n \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y \<in> carrier Zp
\<zero> \<in> carrier Zp
?x \<in> carrier Zp \<Longrightarrow> \<ominus> ?x \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<ominus> ?y \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<in> carrier Zp
\<one> \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y \<oplus> ?z = ?x \<oplus> (?y \<oplus> ?z)
?x \<in> carrier Zp \<Longrightarrow> \<zero> \<oplus> ?x = ?x
?x \<in> carrier Zp \<Longrightarrow> \<ominus> ?x \<oplus> ?x = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y = ?y \<oplus> ?x
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<otimes> ?z = ?x \<otimes> (?y \<otimes> ?z)
?x \<in> carrier Zp \<Longrightarrow> \<one> \<otimes> ?x = ?x
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> (?x \<oplus> ?y) \<otimes> ?z = ?x \<otimes> ?z \<oplus> ?y \<otimes> ?z
?x \<ominus> ?y = ?x \<oplus> \<ominus> ?y
?x \<in> carrier Zp \<Longrightarrow> ?x \<oplus> \<zero> = ?x
?x \<in> carrier Zp \<Longrightarrow> ?x \<oplus> \<ominus> ?x = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> (\<ominus> ?x \<oplus> ?y) = ?y
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> ?x \<oplus> (?x \<oplus> ?y) = ?y
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> (?x \<oplus> ?y) = \<ominus> ?x \<oplus> \<ominus> ?y
?x \<in> carrier Zp \<Longrightarrow> \<ominus> (\<ominus> ?x) = ?x
\<ominus> \<zero> = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> (?y \<oplus> ?z) = ?y \<oplus> (?x \<oplus> ?z)
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?z \<otimes> (?x \<oplus> ?y) = ?z \<otimes> ?x \<oplus> ?z \<otimes> ?y
?x \<in> carrier Zp \<Longrightarrow> \<zero> \<otimes> ?x = \<zero>
?x \<in> carrier Zp \<Longrightarrow> ?x \<otimes> \<zero> = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> ?x \<otimes> ?y = \<ominus> (?x \<otimes> ?y)
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<otimes> \<ominus> ?y = \<ominus> (?x \<otimes> ?y)

goal (1 subgoal):
 1. ns (Suc n) \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
[PROOF STEP]
unfolding newton_step_def a_minus_def
[PROOF STATE]
proof (prove)
using this:
ns (Suc n) = ns n \<oplus> \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
local.divide (f \<bullet> ns n) (f' \<bullet> ns n) \<in> carrier Zp
ns (Suc n) \<in> carrier Zp
ns n \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y \<in> carrier Zp
\<zero> \<in> carrier Zp
?x \<in> carrier Zp \<Longrightarrow> \<ominus> ?x \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> \<ominus> ?y \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<in> carrier Zp
\<one> \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y \<oplus> ?z = ?x \<oplus> (?y \<oplus> ?z)
?x \<in> carrier Zp \<Longrightarrow> \<zero> \<oplus> ?x = ?x
?x \<in> carrier Zp \<Longrightarrow> \<ominus> ?x \<oplus> ?x = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y = ?y \<oplus> ?x
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<otimes> ?z = ?x \<otimes> (?y \<otimes> ?z)
?x \<in> carrier Zp \<Longrightarrow> \<one> \<otimes> ?x = ?x
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> (?x \<oplus> ?y) \<otimes> ?z = ?x \<otimes> ?z \<oplus> ?y \<otimes> ?z
?x \<oplus> \<ominus> ?y = ?x \<oplus> \<ominus> ?y
?x \<in> carrier Zp \<Longrightarrow> ?x \<oplus> \<zero> = ?x
?x \<in> carrier Zp \<Longrightarrow> ?x \<oplus> \<ominus> ?x = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> (\<ominus> ?x \<oplus> ?y) = ?y
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> ?x \<oplus> (?x \<oplus> ?y) = ?y
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> (?x \<oplus> ?y) = \<ominus> ?x \<oplus> \<ominus> ?y
?x \<in> carrier Zp \<Longrightarrow> \<ominus> (\<ominus> ?x) = ?x
\<ominus> \<zero> = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> (?y \<oplus> ?z) = ?y \<oplus> (?x \<oplus> ?z)
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?z \<otimes> (?x \<oplus> ?y) = ?z \<otimes> ?x \<oplus> ?z \<otimes> ?y
?x \<in> carrier Zp \<Longrightarrow> \<zero> \<otimes> ?x = \<zero>
?x \<in> carrier Zp \<Longrightarrow> ?x \<otimes> \<zero> = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> ?x \<otimes> ?y = \<ominus> (?x \<otimes> ?y)
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<otimes> \<ominus> ?y = \<ominus> (?x \<otimes> ?y)

goal (1 subgoal):
 1. ns (Suc n) \<oplus> \<ominus> ns n = \<ominus> local.divide (f \<bullet> ns n) (f' \<bullet> ns n)
[PROOF STEP]
by smt


[STATEMENT]
lemma newton_seq_fact8:
  assumes "f\<bullet>(ns l) \<noteq>\<zero>"
  shows "divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> nonzero Zp
[PROOF STEP]
using assms divide_nonzero[of "f \<bullet> ns l" "f' \<bullet> ns l"]
        nonzero_memI
[PROOF STATE]
proof (prove)
using this:
f \<bullet> ns l \<noteq> \<zero>
\<lbrakk>f \<bullet> ns l \<in> nonzero Zp; f' \<bullet> ns l \<in> nonzero Zp; val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)\<rbrakk> \<Longrightarrow> local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> nonzero Zp
\<lbrakk>?a \<in> carrier Zp; ?a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ?a \<in> nonzero Zp

goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> nonzero Zp
[PROOF STEP]
using f_of_newton_seq_closed newton_seq_fact3 newton_seq_fact6
[PROOF STATE]
proof (prove)
using this:
f \<bullet> ns l \<noteq> \<zero>
\<lbrakk>f \<bullet> ns l \<in> nonzero Zp; f' \<bullet> ns l \<in> nonzero Zp; val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)\<rbrakk> \<Longrightarrow> local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> nonzero Zp
\<lbrakk>?a \<in> carrier Zp; ?a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ?a \<in> nonzero Zp
f \<bullet> ns ?m \<in> carrier Zp
val_Zp (f' \<bullet> ns ?l) \<le> val_Zp (f \<bullet> ns ?l)
f' \<bullet> ns ?l \<in> nonzero Zp

goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> nonzero Zp
[PROOF STEP]
by blast


[STATEMENT]
lemma newton_seq_fact9:
  assumes "f\<bullet>(ns n) \<noteq>\<zero>"
  shows "val_Zp((ns (Suc n)) \<ominus> (ns n)) = val_Zp (f\<bullet>(ns n)) - val_Zp (f'\<bullet>(ns n))"
[PROOF STATE]
proof (prove)
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 newton_seq_fact7 val_of_divide newton_seq_fact6 assms nonzero_memI
        f_of_newton_seq_closed newton_seq_fact4 newton_seq_fact5
[PROOF STATE]
proof (prove)
using this:
ns (Suc ?n) \<ominus> ns ?n = \<ominus> local.divide (f \<bullet> ns ?n) (f' \<bullet> ns ?n)
\<lbrakk>?x \<in> carrier Zp; ?y \<in> nonzero Zp; val_Zp ?y \<le> val_Zp ?x\<rbrakk> \<Longrightarrow> val_Zp (local.divide ?x ?y) = val_Zp ?x - val_Zp ?y
f' \<bullet> ns ?l \<in> nonzero Zp
f \<bullet> ns n \<noteq> \<zero>
\<lbrakk>?a \<in> carrier Zp; ?a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ?a \<in> nonzero Zp
f \<bullet> ns ?m \<in> carrier Zp
f \<bullet> ns ?l \<noteq> \<zero> \<Longrightarrow> val_Zp (f' \<bullet> ns ?l) \<le> val_Zp (f \<bullet> ns ?l)
local.divide (f \<bullet> ns ?l) (f' \<bullet> ns ?l) \<in> carrier Zp

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 (metis val_Zp_of_minus)


[STATEMENT]
lemma newton_seq_is_Zp_cauchy_0:
assumes "\<And>k. f\<bullet>(ns k) \<noteq>\<zero>"
shows "is_Zp_cauchy ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_Zp_cauchy ns
[PROOF STEP]
proof(rule is_Zp_cauchyI')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ns \<in> carrier Zp\<^bsup>\<omega>\<^esup>
 2. \<forall>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
show P0: "ns \<in> closed_seqs Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns \<in> carrier Zp\<^bsup>\<omega>\<^esup>
[PROOF STEP]
proof(rule closed_seqs_memI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. ns k \<in> carrier Zp
[PROOF STEP]
show "\<And>k. ns k \<in> carrier Zp "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. ns k \<in> carrier Zp
[PROOF STEP]
by (simp add: newton_seq_closed)
[PROOF STATE]
proof (state)
this:
ns ?k2 \<in> carrier Zp

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns \<in> carrier Zp\<^bsup>\<omega>\<^esup>

goal (1 subgoal):
 1. \<forall>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
show "\<forall>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> int n \<le> val_Zp (ns (Suc m) \<ominus> ns m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
show "\<exists>k. \<forall>m. k \<le> int m \<longrightarrow> int n \<le> val_Zp (ns (Suc m) \<ominus> ns m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
proof(induction "n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
 2. \<And>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m) \<Longrightarrow> \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
 2. \<And>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m) \<Longrightarrow> \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
have B0: "\<forall>n0 n1. 0 < n0 \<and> 0 < n1 \<longrightarrow> ns n0 0 = ns n1 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n0 n1. 0 < n0 \<and> 0 < n1 \<longrightarrow> ns n0 0 = ns n1 0
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n0 n1. \<lbrakk>0 < n0; 0 < n1\<rbrakk> \<Longrightarrow> ns n0 0 = ns n1 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n0 n1. \<lbrakk>0 < n0; 0 < n1\<rbrakk> \<Longrightarrow> ns n0 0 = ns n1 0
[PROOF STEP]
fix n0 n1::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n0 n1. \<lbrakk>0 < n0; 0 < n1\<rbrakk> \<Longrightarrow> ns n0 0 = ns n1 0
[PROOF STEP]
assume A: "0 < n0" "0 < n1"
[PROOF STATE]
proof (state)
this:
0 < n0
0 < n1

goal (1 subgoal):
 1. \<And>n0 n1. \<lbrakk>0 < n0; 0 < n1\<rbrakk> \<Longrightarrow> ns n0 0 = ns n1 0
[PROOF STEP]
show "ns n0 0 = ns n1 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns n0 0 = ns n1 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns n0 0 = ns n1 0
[PROOF STEP]
have 0: "ns n0 \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns n0 \<in> carrier Zp
[PROOF STEP]
using P0
[PROOF STATE]
proof (prove)
using this:
ns \<in> carrier Zp\<^bsup>\<omega>\<^esup>

goal (1 subgoal):
 1. ns n0 \<in> carrier Zp
[PROOF STEP]
by (simp add: newton_seq_closed)
[PROOF STATE]
proof (state)
this:
ns n0 \<in> carrier Zp

goal (1 subgoal):
 1. ns n0 0 = ns n1 0
[PROOF STEP]
have 1: "ns n1 \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns n1 \<in> carrier Zp
[PROOF STEP]
using P0
[PROOF STATE]
proof (prove)
using this:
ns \<in> carrier Zp\<^bsup>\<omega>\<^esup>

goal (1 subgoal):
 1. ns n1 \<in> carrier Zp
[PROOF STEP]
by (simp add: newton_seq_closed)
[PROOF STATE]
proof (state)
this:
ns n1 \<in> carrier Zp

goal (1 subgoal):
 1. ns n0 0 = ns n1 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns n0 0 = ns n1 0
[PROOF STEP]
using 0 1 Zp_defs(3) prime
[PROOF STATE]
proof (prove)
using this:
ns n0 \<in> carrier Zp
ns n1 \<in> carrier Zp
carrier Zp = padic_set p
prime p

goal (1 subgoal):
 1. ns n0 0 = ns n1 0
[PROOF STEP]
by (metis p_res_ring_0' residue_closed)
[PROOF STATE]
proof (state)
this:
ns n0 0 = ns n1 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns n0 0 = ns n1 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n0 n1. 0 < n0 \<and> 0 < n1 \<longrightarrow> ns n0 0 = ns n1 0

goal (2 subgoals):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
 2. \<And>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m) \<Longrightarrow> \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
have "\<forall>m. 1 \<le> int m \<longrightarrow> int 0 \<le> val_Zp_dist (newton_step (ns m)) (ns m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m. 1 \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. 1 \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. 1 \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
show "1 \<le> int m \<longrightarrow> int 0 \<le> val_Zp_dist (newton_step (ns m)) (ns m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> int m \<Longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
assume "1 \<le> int m "
[PROOF STATE]
proof (state)
this:
1 \<le> int m

goal (1 subgoal):
 1. 1 \<le> int m \<Longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> int m
[PROOF STEP]
have C0:"ns (Suc m) 0 = ns m 0"
[PROOF STATE]
proof (prove)
using this:
1 \<le> int m

goal (1 subgoal):
 1. ns (Suc m) 0 = ns m 0
[PROOF STEP]
using B0
[PROOF STATE]
proof (prove)
using this:
1 \<le> int m
\<forall>n0 n1. 0 < n0 \<and> 0 < n1 \<longrightarrow> ns n0 0 = ns n1 0

goal (1 subgoal):
 1. ns (Suc m) 0 = ns m 0
[PROOF STEP]
by (metis int_one_le_iff_zero_less int_ops(1) less_Suc_eq_0_disj of_nat_less_iff)
[PROOF STATE]
proof (state)
this:
ns (Suc m) 0 = ns m 0

goal (1 subgoal):
 1. 1 \<le> int m \<Longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ns (Suc m) 0 = ns m 0
[PROOF STEP]
show "int 0 \<le> val_Zp_dist (newton_step (ns m)) (ns m)"
[PROOF STATE]
proof (prove)
using this:
ns (Suc m) 0 = ns m 0

goal (1 subgoal):
 1. eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns (Suc m) 0 = ns m 0 \<Longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
have "(newton_step (ns m)) \<noteq>(ns m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. newton_step (ns m) \<noteq> ns m
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. newton_step (ns m) \<noteq> ns m
[PROOF STEP]
have A0: "divide (f\<bullet>(ns m)) (f'\<bullet>(ns m)) \<noteq>\<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<noteq> \<zero>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<noteq> \<zero>
[PROOF STEP]
have 0: "(f\<bullet>(ns m)) \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> ns m \<noteq> \<zero>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<bullet> ns ?k2 \<noteq> \<zero>

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

goal (1 subgoal):
 1. local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<noteq> \<zero>
[PROOF STEP]
have 1: " (f'\<bullet>(ns m)) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> ns m \<in> carrier Zp
[PROOF STEP]
by (simp add: UP_cring.to_fun_closed Zp_x_is_UP_cring f'_closed newton_seq_closed)
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns m \<in> carrier Zp

goal (1 subgoal):
 1. local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<noteq> \<zero>
[PROOF STEP]
have 2:  "(f'\<bullet>(ns m)) \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> ns m \<noteq> \<zero>
[PROOF STEP]
using newton_seq_fact6 not_nonzero_memI
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> ns ?l \<in> nonzero Zp
?a = \<zero> \<Longrightarrow> ?a \<notin> nonzero Zp

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

goal (1 subgoal):
 1. local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<noteq> \<zero>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<noteq> \<zero>
[PROOF STEP]
using 0 1 2
[PROOF STATE]
proof (prove)
using this:
f \<bullet> ns m \<noteq> \<zero>
f' \<bullet> ns m \<in> carrier Zp
f' \<bullet> ns m \<noteq> \<zero>

goal (1 subgoal):
 1. local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<noteq> \<zero>
[PROOF STEP]
by (metis R.r_null divide_formula f_closed to_fun_closed newton_seq_closed newton_seq_fact4)
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<noteq> \<zero>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<noteq> \<zero>

goal (1 subgoal):
 1. newton_step (ns m) \<noteq> ns m
[PROOF STEP]
have A2: "local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<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 m) (f' \<bullet> ns m) \<in> carrier Zp
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<in> carrier Zp

goal (1 subgoal):
 1. newton_step (ns m) \<noteq> ns m
[PROOF STEP]
have A3: "ns m \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns m \<in> carrier Zp
[PROOF STEP]
by (simp add: newton_seq_closed)
[PROOF STATE]
proof (state)
this:
ns m \<in> carrier Zp

goal (1 subgoal):
 1. newton_step (ns m) \<noteq> ns m
[PROOF STEP]
have A4: "newton_step (ns m) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. newton_step (ns m) \<in> carrier Zp
[PROOF STEP]
by (metis newton_seq.simps(2) newton_seq_closed)
[PROOF STATE]
proof (state)
this:
newton_step (ns m) \<in> carrier Zp

goal (1 subgoal):
 1. newton_step (ns m) \<noteq> ns m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. newton_step (ns m) \<noteq> ns m
[PROOF STEP]
apply(rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> newton_step (ns m) \<noteq> ns m \<Longrightarrow> False
[PROOF STEP]
using A4 A3 A2 A0 newton_step_def[of "(ns m)"]
[PROOF STATE]
proof (prove)
using this:
newton_step (ns m) \<in> carrier Zp
ns m \<in> carrier Zp
local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<in> carrier Zp
local.divide (f \<bullet> ns m) (f' \<bullet> ns m) \<noteq> \<zero>
newton_step (ns m) = ns m \<ominus> local.divide (f \<bullet> ns m) (f' \<bullet> ns m)

goal (1 subgoal):
 1. \<not> newton_step (ns m) \<noteq> ns m \<Longrightarrow> False
[PROOF STEP]
by (simp add: a_minus_def)
[PROOF STATE]
proof (state)
this:
newton_step (ns m) \<noteq> ns m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
newton_step (ns m) \<noteq> ns m

goal (1 subgoal):
 1. ns (Suc m) 0 = ns m 0 \<Longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
newton_step (ns m) \<noteq> ns m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
newton_step (ns m) \<noteq> ns m

goal (1 subgoal):
 1. eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
using C0
[PROOF STATE]
proof (prove)
using this:
newton_step (ns m) \<noteq> ns m
ns (Suc m) 0 = ns m 0

goal (1 subgoal):
 1. eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
by (metis newton_seq.simps(2) newton_seq_closed val_Zp_dist_res_eq2)
[PROOF STATE]
proof (state)
this:
eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>m. 1 \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)

goal (2 subgoals):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
 2. \<And>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m) \<Longrightarrow> \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m. 1 \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>m. 1 \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)

goal (1 subgoal):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
using val_Zp_def val_Zp_dist_def
[PROOF STATE]
proof (prove)
using this:
\<forall>m. 1 \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
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)

goal (1 subgoal):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
by (metis int_ops(1) newton_seq.simps(2) zero_eint_def)
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int 0) \<le> val_Zp (ns (Suc m) \<ominus> ns m)

goal (1 subgoal):
 1. \<And>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m) \<Longrightarrow> \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m) \<Longrightarrow> \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)

goal (1 subgoal):
 1. \<And>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m) \<Longrightarrow> \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
show "\<exists>k. \<forall>m. k \<le> int m \<longrightarrow> int (Suc n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
obtain k0 where k0_def: "k0 \<ge>0 \<and> (\<forall>m. k0 \<le> int m \<longrightarrow> int n \<le> val_Zp (ns (Suc m) \<ominus> ns m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k0. 0 \<le> k0 \<and> (\<forall>m. k0 \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Suc.IH
[PROOF STATE]
proof (prove)
using this:
\<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)

goal (1 subgoal):
 1. (\<And>k0. 0 \<le> k0 \<and> (\<forall>m. k0 \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis int_nat_eq le0 nat_le_iff of_nat_0_eq_iff )
[PROOF STATE]
proof (state)
this:
0 \<le> k0 \<and> (\<forall>m. k0 \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m))

goal (1 subgoal):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
have I0: "\<And>l. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (f\<bullet> (ns l)) - val_Zp (f'\<bullet>(ns l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)
[PROOF STEP]
have I00:"(ns (Suc l) \<ominus> ns l) = (\<ominus> divide (f\<bullet>(ns l)) (f'\<bullet>(ns l)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns (Suc l) \<ominus> ns l = \<ominus> local.divide (f \<bullet> ns l) (f' \<bullet> ns l)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns (Suc l) \<ominus> ns l = \<ominus> local.divide (f \<bullet> ns l) (f' \<bullet> ns l)
[PROOF STEP]
have "local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp
[PROOF STEP]
by (simp add: newton_seq_fact5)
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp

goal (1 subgoal):
 1. ns (Suc l) \<ominus> ns l = \<ominus> local.divide (f \<bullet> ns l) (f' \<bullet> ns l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp

goal (1 subgoal):
 1. ns (Suc l) \<ominus> ns l = \<ominus> local.divide (f \<bullet> ns l) (f' \<bullet> ns l)
[PROOF STEP]
using newton_seq.simps(2)[of l] newton_seq_closed R.ring_simprules
[PROOF STATE]
proof (prove)
using this:
local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp
ns (Suc l) = newton_step (ns l)
ns ?m \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y \<in> carrier Zp
\<zero> \<in> carrier Zp
?x \<in> carrier Zp \<Longrightarrow> \<ominus> ?x \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<ominus> ?y \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<in> carrier Zp
\<one> \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y \<oplus> ?z = ?x \<oplus> (?y \<oplus> ?z)
?x \<in> carrier Zp \<Longrightarrow> \<zero> \<oplus> ?x = ?x
?x \<in> carrier Zp \<Longrightarrow> \<ominus> ?x \<oplus> ?x = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y = ?y \<oplus> ?x
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<otimes> ?z = ?x \<otimes> (?y \<otimes> ?z)
?x \<in> carrier Zp \<Longrightarrow> \<one> \<otimes> ?x = ?x
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> (?x \<oplus> ?y) \<otimes> ?z = ?x \<otimes> ?z \<oplus> ?y \<otimes> ?z
?x \<ominus> ?y = ?x \<oplus> \<ominus> ?y
?x \<in> carrier Zp \<Longrightarrow> ?x \<oplus> \<zero> = ?x
?x \<in> carrier Zp \<Longrightarrow> ?x \<oplus> \<ominus> ?x = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> (\<ominus> ?x \<oplus> ?y) = ?y
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> ?x \<oplus> (?x \<oplus> ?y) = ?y
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> (?x \<oplus> ?y) = \<ominus> ?x \<oplus> \<ominus> ?y
?x \<in> carrier Zp \<Longrightarrow> \<ominus> (\<ominus> ?x) = ?x
\<ominus> \<zero> = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> (?y \<oplus> ?z) = ?y \<oplus> (?x \<oplus> ?z)
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?z \<otimes> (?x \<oplus> ?y) = ?z \<otimes> ?x \<oplus> ?z \<otimes> ?y
?x \<in> carrier Zp \<Longrightarrow> \<zero> \<otimes> ?x = \<zero>
?x \<in> carrier Zp \<Longrightarrow> ?x \<otimes> \<zero> = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> ?x \<otimes> ?y = \<ominus> (?x \<otimes> ?y)
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<otimes> \<ominus> ?y = \<ominus> (?x \<otimes> ?y)

goal (1 subgoal):
 1. ns (Suc l) \<ominus> ns l = \<ominus> local.divide (f \<bullet> ns l) (f' \<bullet> ns l)
[PROOF STEP]
unfolding newton_step_def a_minus_def
[PROOF STATE]
proof (prove)
using this:
local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp
ns (Suc l) = ns l \<oplus> \<ominus> local.divide (f \<bullet> ns l) (f' \<bullet> ns l)
ns ?m \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y \<in> carrier Zp
\<zero> \<in> carrier Zp
?x \<in> carrier Zp \<Longrightarrow> \<ominus> ?x \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> \<ominus> ?y \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<in> carrier Zp
\<one> \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y \<oplus> ?z = ?x \<oplus> (?y \<oplus> ?z)
?x \<in> carrier Zp \<Longrightarrow> \<zero> \<oplus> ?x = ?x
?x \<in> carrier Zp \<Longrightarrow> \<ominus> ?x \<oplus> ?x = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y = ?y \<oplus> ?x
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<otimes> ?z = ?x \<otimes> (?y \<otimes> ?z)
?x \<in> carrier Zp \<Longrightarrow> \<one> \<otimes> ?x = ?x
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> (?x \<oplus> ?y) \<otimes> ?z = ?x \<otimes> ?z \<oplus> ?y \<otimes> ?z
?x \<oplus> \<ominus> ?y = ?x \<oplus> \<ominus> ?y
?x \<in> carrier Zp \<Longrightarrow> ?x \<oplus> \<zero> = ?x
?x \<in> carrier Zp \<Longrightarrow> ?x \<oplus> \<ominus> ?x = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> (\<ominus> ?x \<oplus> ?y) = ?y
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> ?x \<oplus> (?x \<oplus> ?y) = ?y
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> (?x \<oplus> ?y) = \<ominus> ?x \<oplus> \<ominus> ?y
?x \<in> carrier Zp \<Longrightarrow> \<ominus> (\<ominus> ?x) = ?x
\<ominus> \<zero> = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<oplus> (?y \<oplus> ?z) = ?y \<oplus> (?x \<oplus> ?z)
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?z \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?z \<otimes> (?x \<oplus> ?y) = ?z \<otimes> ?x \<oplus> ?z \<otimes> ?y
?x \<in> carrier Zp \<Longrightarrow> \<zero> \<otimes> ?x = \<zero>
?x \<in> carrier Zp \<Longrightarrow> ?x \<otimes> \<zero> = \<zero>
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> \<ominus> ?x \<otimes> ?y = \<ominus> (?x \<otimes> ?y)
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?x \<otimes> \<ominus> ?y = \<ominus> (?x \<otimes> ?y)

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

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

goal (1 subgoal):
 1. \<And>l. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)
[PROOF STEP]
have I01: "val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (divide (f\<bullet>(ns l)) (f'\<bullet>(ns l)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (local.divide (f \<bullet> ns l) (f' \<bullet> ns l))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (local.divide (f \<bullet> ns l) (f' \<bullet> ns l))
[PROOF STEP]
have I010: "(divide (f\<bullet>(ns l)) (f'\<bullet>(ns l))) \<in>carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp
[PROOF STEP]
by (simp add: newton_seq_fact5)
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp

goal (1 subgoal):
 1. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (local.divide (f \<bullet> ns l) (f' \<bullet> ns l))
[PROOF STEP]
have I011: "(divide (f\<bullet>(ns l)) (f'\<bullet>(ns l))) \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<noteq> \<zero>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<noteq> \<zero>
[PROOF STEP]
have A: "(f\<bullet>(ns l)) \<noteq>\<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> ns l \<noteq> \<zero>
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
f \<bullet> ns l \<noteq> \<zero>

goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<noteq> \<zero>
[PROOF STEP]
have B: " (f'\<bullet>(ns l))  \<in>carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> ns l \<in> carrier Zp
[PROOF STEP]
using nonzero_memE newton_seq_fact6
[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 ?l \<in> nonzero Zp

goal (1 subgoal):
 1. f' \<bullet> ns l \<in> carrier Zp
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns l \<in> carrier Zp

goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<noteq> \<zero>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f' \<bullet> ns l \<in> carrier Zp
[PROOF STEP]
have C: " (f'\<bullet>(ns l))  \<in>nonzero  Zp"
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> ns l \<in> carrier Zp

goal (1 subgoal):
 1. f' \<bullet> ns l \<in> nonzero Zp
[PROOF STEP]
using  f'a_closed fa_closed fa_nonzero hensel_factor_id hensel_hypothesis_weakened
                     newton_seq_fact1[of l]   not_nonzero_Zp val_Zp_def
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> ns l \<in> carrier Zp
f' \<bullet> a \<in> carrier Zp
f \<bullet> a \<in> carrier Zp
f \<bullet> a \<noteq> \<zero>
local.divide (f \<bullet> a) (f' \<bullet> a) \<otimes> (f' \<bullet> a) = f \<bullet> a
val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)
val_Zp (f' \<bullet> ns l) = val_Zp (f' \<bullet> a)
\<lbrakk>?x \<in> carrier Zp; ?x \<notin> nonzero Zp\<rbrakk> \<Longrightarrow> ?x = \<zero>
val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))

goal (1 subgoal):
 1. f' \<bullet> ns l \<in> nonzero Zp
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns l \<in> nonzero Zp

goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<noteq> \<zero>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f' \<bullet> ns l \<in> nonzero Zp
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> ns l \<in> nonzero Zp

goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<noteq> \<zero>
[PROOF STEP]
using I010 A
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> ns l \<in> nonzero Zp
local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp
f \<bullet> ns l \<noteq> \<zero>

goal (1 subgoal):
 1. local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<noteq> \<zero>
[PROOF STEP]
by (metis B R.r_null divide_formula f_closed to_fun_closed newton_seq_closed newton_seq_fact4 nonzero_memE(2))
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<noteq> \<zero>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<noteq> \<zero>

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

goal (1 subgoal):
 1. val_Zp (local.divide (f \<bullet> ns l) (f' \<bullet> ns l)) = val_Zp (\<ominus> local.divide (f \<bullet> ns l) (f' \<bullet> ns l))
[PROOF STEP]
using I010 not_nonzero_Zp val_Zp_of_minus
[PROOF STATE]
proof (prove)
using this:
local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<noteq> \<zero>
local.divide (f \<bullet> ns l) (f' \<bullet> ns l) \<in> carrier Zp
\<lbrakk>?x \<in> carrier Zp; ?x \<notin> nonzero Zp\<rbrakk> \<Longrightarrow> ?x = \<zero>
?a \<in> carrier Zp \<Longrightarrow> val_Zp ?a = val_Zp (\<ominus> ?a)

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

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

goal (1 subgoal):
 1. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (local.divide (f \<bullet> ns l) (f' \<bullet> ns l))
[PROOF STEP]
using I00
[PROOF STATE]
proof (prove)
using this:
val_Zp (local.divide (f \<bullet> ns l) (f' \<bullet> ns l)) = val_Zp (\<ominus> local.divide (f \<bullet> ns l) (f' \<bullet> ns l))
ns (Suc l) \<ominus> ns l = \<ominus> local.divide (f \<bullet> ns l) (f' \<bullet> ns l)

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

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

goal (1 subgoal):
 1. \<And>l. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)
[PROOF STEP]
have I02: "val_Zp (f\<bullet>(ns l)) \<ge> val_Zp (f'\<bullet>(ns l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)
[PROOF STEP]
using assms  newton_seq_fact4
[PROOF STATE]
proof (prove)
using this:
f \<bullet> ns ?k2 \<noteq> \<zero>
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 l) \<le> val_Zp (f \<bullet> ns l)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)

goal (1 subgoal):
 1. \<And>l. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)
[PROOF STEP]
have I03: "(f\<bullet>(ns l)) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> ns l \<in> nonzero Zp
[PROOF STEP]
by (meson UP_cring.to_fun_closed Zp_x_is_UP_cring assms f_closed newton_seq_closed not_nonzero_Zp)
[PROOF STATE]
proof (state)
this:
f \<bullet> ns l \<in> nonzero Zp

goal (1 subgoal):
 1. \<And>l. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)
[PROOF STEP]
have I04: "f'\<bullet>(ns l) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> ns l \<in> nonzero Zp
[PROOF STEP]
by (simp add: newton_seq_fact6)
[PROOF STATE]
proof (state)
this:
f' \<bullet> ns l \<in> nonzero Zp

goal (1 subgoal):
 1. \<And>l. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)
[PROOF STEP]
have I05 :" val_Zp (divide (f\<bullet>(ns l)) (f'\<bullet>(ns l))) = val_Zp (f\<bullet> (ns l)) - val_Zp (f'\<bullet>(ns l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (local.divide (f \<bullet> ns l) (f' \<bullet> ns l)) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)
[PROOF STEP]
using I02 I03 I04 I01 assms newton_seq_fact9
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns l) \<le> val_Zp (f \<bullet> ns l)
f \<bullet> ns l \<in> nonzero Zp
f' \<bullet> ns l \<in> nonzero Zp
val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (local.divide (f \<bullet> ns l) (f' \<bullet> ns l))
f \<bullet> ns ?k2 \<noteq> \<zero>
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)

goal (1 subgoal):
 1. val_Zp (local.divide (f \<bullet> ns l) (f' \<bullet> ns l)) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp (local.divide (f \<bullet> ns l) (f' \<bullet> ns l)) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)

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

goal (1 subgoal):
 1. val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)
[PROOF STEP]
using I01
[PROOF STATE]
proof (prove)
using this:
val_Zp (local.divide (f \<bullet> ns l) (f' \<bullet> ns l)) = val_Zp (f \<bullet> ns l) - val_Zp (f' \<bullet> ns l)
val_Zp (ns (Suc l) \<ominus> ns l) = val_Zp (local.divide (f \<bullet> ns l) (f' \<bullet> ns l))

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

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

goal (1 subgoal):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
have "\<forall>m. int(Suc n) + k0 + 1 \<le> int m \<longrightarrow> int (Suc n) \<le> val_Zp_dist (newton_step (ns m)) (ns m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m. int (Suc n) + k0 + 1 \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. int (Suc n) + k0 + 1 \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. int (Suc n) + k0 + 1 \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
show "int (Suc n) + k0 + 1 \<le> int m \<longrightarrow> int (Suc n) \<le> val_Zp_dist (newton_step (ns m)) (ns m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (Suc n) + k0 + 1 \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. int (Suc n) + k0 + 1 \<le> int m \<Longrightarrow> eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
assume A: "int (Suc n) + k0 + 1 \<le> int m "
[PROOF STATE]
proof (state)
this:
int (Suc n) + k0 + 1 \<le> int m

goal (1 subgoal):
 1. int (Suc n) + k0 + 1 \<le> int m \<Longrightarrow> eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
show " int (Suc n) \<le> val_Zp_dist (newton_step (ns m)) (ns m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
have 0: " val_Zp_dist (newton_step (ns m)) (ns m) =  val_Zp (f\<bullet> (ns m)) - val_Zp (f'\<bullet>(ns m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp_dist (newton_step (ns m)) (ns m) = val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
using I0 val_Zp_dist_def
[PROOF STATE]
proof (prove)
using this:
val_Zp (ns (Suc ?l2) \<ominus> ns ?l2) = val_Zp (f \<bullet> ns ?l2) - val_Zp (f' \<bullet> ns ?l2)
val_Zp_dist ?a ?b \<equiv> val_Zp (?a \<ominus> ?b)

goal (1 subgoal):
 1. val_Zp_dist (newton_step (ns m)) (ns m) = val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp_dist (newton_step (ns m)) (ns m) = val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)

goal (1 subgoal):
 1. eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
have 1: "val_Zp (f\<bullet> (ns m)) - val_Zp (f'\<bullet>(ns m)) > int n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
have "val_Zp (f\<bullet> (ns m)) \<ge> 2*(val_Zp (f'\<bullet>a)) + (2^m)*t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ m) * t \<le> val_Zp (f \<bullet> ns m)
[PROOF STEP]
by (simp add: newton_seq_fact2)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ m) * t \<le> val_Zp (f \<bullet> ns m)

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

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

goal (1 subgoal):
 1. eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
have "2^m * t > m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint (int m) < eint (2 ^ m) * t
[PROOF STEP]
apply(induction m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. eint (int 0) < eint (2 ^ 0) * t
 2. \<And>m. eint (int m) < eint (2 ^ m) * t \<Longrightarrow> eint (int (Suc m)) < eint (2 ^ Suc m) * t
[PROOF STEP]
using one_eint_def zero_eint_def
[PROOF STATE]
proof (prove)
using this:
1 = eint 1
0 = eint 0

goal (2 subgoals):
 1. eint (int 0) < eint (2 ^ 0) * t
 2. \<And>m. eint (int m) < eint (2 ^ m) * t \<Longrightarrow> eint (int (Suc m)) < eint (2 ^ Suc m) * t
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. eint (int m) < eint (2 ^ m) * t \<Longrightarrow> eint (int (Suc m)) < eint (2 ^ Suc m) * t
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. eint (int m) < eint (2 ^ m) * t \<Longrightarrow> eint (int (Suc m)) < eint (2 ^ Suc m) * t
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. eint (int m) < eint (2 ^ m) * t \<Longrightarrow> eint (int (Suc m)) < eint (2 ^ Suc m) * t
[PROOF STEP]
assume IH : "int m < 2 ^ m * t "
[PROOF STATE]
proof (state)
this:
eint (int m) < eint (2 ^ m) * t

goal (1 subgoal):
 1. \<And>m. eint (int m) < eint (2 ^ m) * t \<Longrightarrow> eint (int (Suc m)) < eint (2 ^ Suc m) * t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint (int m) < eint (2 ^ m) * t
[PROOF STEP]
have "((2 ^ (Suc m)) * t) = 2* ((2 ^ m) * t)"
[PROOF STATE]
proof (prove)
using this:
eint (int m) < eint (2 ^ m) * t

goal (1 subgoal):
 1. eint (2 ^ Suc m) * t = eint 2 * (eint (2 ^ m) * t)
[PROOF STEP]
by (metis mult.assoc power_Suc times_eint_simps(1))
[PROOF STATE]
proof (state)
this:
eint (2 ^ Suc m) * t = eint 2 * (eint (2 ^ m) * t)

goal (1 subgoal):
 1. \<And>m. eint (int m) < eint (2 ^ m) * t \<Longrightarrow> eint (int (Suc m)) < eint (2 ^ Suc m) * t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint (2 ^ Suc m) * t = eint 2 * (eint (2 ^ m) * t)
[PROOF STEP]
show "int (Suc m) < 2 ^ Suc m * t"
[PROOF STATE]
proof (prove)
using this:
eint (2 ^ Suc m) * t = eint 2 * (eint (2 ^ m) * t)

goal (1 subgoal):
 1. eint (int (Suc m)) < eint (2 ^ Suc m) * t
[PROOF STEP]
using IH t_neq_infty
[PROOF STATE]
proof (prove)
using this:
eint (2 ^ Suc m) * t = eint 2 * (eint (2 ^ m) * t)
eint (int m) < eint (2 ^ m) * t
t \<noteq> \<infinity>

goal (1 subgoal):
 1. eint (int (Suc m)) < eint (2 ^ Suc m) * t
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
eint (int (Suc m)) < eint (2 ^ Suc m) * t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint (int m) < eint (2 ^ m) * t

goal (1 subgoal):
 1. eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint (int m) < eint (2 ^ m) * t
[PROOF STEP]
have 100: "2^m * t > int m"
[PROOF STATE]
proof (prove)
using this:
eint (int m) < eint (2 ^ m) * t

goal (1 subgoal):
 1. eint (int m) < eint (2 ^ m) * t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eint (int m) < eint (2 ^ m) * t

goal (1 subgoal):
 1. eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
have "int m \<ge>2 + (int n + k0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 + (int n + k0) \<le> int m
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
int (Suc n) + k0 + 1 \<le> int m

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

goal (1 subgoal):
 1. eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
hence 1000: "2^m * t > 2 + (int n + k0)"
[PROOF STATE]
proof (prove)
using this:
2 + (int n + k0) \<le> int m

goal (1 subgoal):
 1. eint (2 + (int n + k0)) < eint (2 ^ m) * t
[PROOF STEP]
using 100
[PROOF STATE]
proof (prove)
using this:
2 + (int n + k0) \<le> int m
eint (int m) < eint (2 ^ m) * t

goal (1 subgoal):
 1. eint (2 + (int n + k0)) < eint (2 ^ m) * t
[PROOF STEP]
by (meson eint_ord_simps(2) less_le_trans linorder_not_less)
[PROOF STATE]
proof (state)
this:
eint (2 + (int n + k0)) < eint (2 ^ m) * t

goal (1 subgoal):
 1. eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
have "2 + (int n + k0) > 1 + int n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + int n < 2 + (int n + k0)
[PROOF STEP]
using k0_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> k0 \<and> (\<forall>m. k0 \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m))

goal (1 subgoal):
 1. 1 + int n < 2 + (int n + k0)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
1 + int n < 2 + (int n + k0)

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

goal (1 subgoal):
 1. eint (1 + int n) < eint (2 ^ m) * t
[PROOF STEP]
using 1000  eint_ord_simps(2) k0_def less_le_trans linorder_not_less
[PROOF STATE]
proof (prove)
using this:
1 + int n < 2 + (int n + k0)
eint (2 + (int n + k0)) < eint (2 ^ m) * t
(eint ?m < eint ?n) = (?m < ?n)
0 \<le> k0 \<and> (\<forall>m. k0 \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m))
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. eint (1 + int n) < eint (2 ^ m) * t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>1 + int n < 2 + (int n + k0); eint (2 + (int n + k0)) < eint (2 ^ m) * t; \<And>m n. (eint m < eint n) = (m < n); 0 \<le> k0 \<and> (\<forall>m. k0 \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)); \<And>x y z. \<lbrakk>x < y; y \<le> z\<rbrakk> \<Longrightarrow> x < z; \<And>x y. (\<not> x < y) = (y \<le> x)\<rbrakk> \<Longrightarrow> eint (1 + int n) < eint (2 ^ m) * t
[PROOF STEP]
have "eint (2 + (int n + k0)) < t * eint (int (2 ^ m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint (2 + (int n + k0)) < t * eint (int (2 ^ m))
[PROOF STEP]
by (metis "1000" mult.commute numeral_power_eq_of_nat_cancel_iff)
[PROOF STATE]
proof (state)
this:
eint (2 + (int n + k0)) < t * eint (int (2 ^ m))

goal (1 subgoal):
 1. \<lbrakk>1 + int n < 2 + (int n + k0); eint (2 + (int n + k0)) < eint (2 ^ m) * t; \<And>m n. (eint m < eint n) = (m < n); 0 \<le> k0 \<and> (\<forall>m. k0 \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)); \<And>x y z. \<lbrakk>x < y; y \<le> z\<rbrakk> \<Longrightarrow> x < z; \<And>x y. (\<not> x < y) = (y \<le> x)\<rbrakk> \<Longrightarrow> eint (1 + int n) < eint (2 ^ m) * t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint (2 + (int n + k0)) < t * eint (int (2 ^ m))
[PROOF STEP]
have "eint (int (Suc n)) < t * eint (int (2 ^ m))"
[PROOF STATE]
proof (prove)
using this:
eint (2 + (int n + k0)) < t * eint (int (2 ^ m))

goal (1 subgoal):
 1. eint (int (Suc n)) < t * eint (int (2 ^ m))
[PROOF STEP]
by (metis \<open>1 + int n < 2 + (int n + k0)\<close> eint_ord_simps(2) less_trans of_nat_Suc)
[PROOF STATE]
proof (state)
this:
eint (int (Suc n)) < t * eint (int (2 ^ m))

goal (1 subgoal):
 1. \<lbrakk>1 + int n < 2 + (int n + k0); eint (2 + (int n + k0)) < eint (2 ^ m) * t; \<And>m n. (eint m < eint n) = (m < n); 0 \<le> k0 \<and> (\<forall>m. k0 \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)); \<And>x y z. \<lbrakk>x < y; y \<le> z\<rbrakk> \<Longrightarrow> x < z; \<And>x y. (\<not> x < y) = (y \<le> x)\<rbrakk> \<Longrightarrow> eint (1 + int n) < eint (2 ^ m) * t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint (int (Suc n)) < t * eint (int (2 ^ m))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eint (int (Suc n)) < t * eint (int (2 ^ m))

goal (1 subgoal):
 1. eint (1 + int n) < eint (2 ^ m) * t
[PROOF STEP]
by (simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
eint (1 + int n) < eint (2 ^ m) * t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint (1 + int n) < eint (2 ^ m) * t

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

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + 1 + eint (int n) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ m) * t
[PROOF STEP]
by (smt eSuc_eint eint_add_left_cancel_le iadd_Suc iadd_Suc_right order_less_le)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + 1 + eint (int n) \<le> eint 2 * val_Zp (f' \<bullet> a) + eint (2 ^ m) * t

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

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

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + 1 + eint (int n) - val_Zp (f' \<bullet> ns m) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
by (smt \<open>eint 2 * val_Zp (f'\<bullet>a) + eint (2 ^ m) * t \<le> val_Zp (to_fun f (ns m))\<close>
                    f'a_not_infinite eint_minus_ineq hensel_axioms newton_seq_fact1 order_trans)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + 1 + eint (int n) - val_Zp (f' \<bullet> ns m) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)

goal (1 subgoal):
 1. eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
have 12: "val_Zp (f'\<bullet>(ns m))  = val_Zp (f'\<bullet>a) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> ns m) = val_Zp (f' \<bullet> a)
[PROOF STEP]
using nonzero_memE  newton_seq_fact1 newton_seq_fact6 val_Zp_def val_Zp_def
[PROOF STATE]
proof (prove)
using this:
?a \<in> nonzero Zp \<Longrightarrow> ?a \<in> carrier Zp
?a \<in> nonzero Zp \<Longrightarrow> ?a \<noteq> \<zero>
val_Zp (f' \<bullet> ns ?k) = val_Zp (f' \<bullet> a)
f' \<bullet> ns ?l \<in> nonzero Zp
val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))
val_Zp = (\<lambda>x. if x = \<zero> then \<infinity> else eint (padic_val p x))

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

goal (1 subgoal):
 1. eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f' \<bullet> ns m) = val_Zp (f' \<bullet> a)
[PROOF STEP]
have 13: "val_Zp (f\<bullet> (ns m)) - val_Zp (f'\<bullet>(ns m))
                                \<ge> 2*(val_Zp (f'\<bullet>a)) + (1 + int n) -  val_Zp ((f'\<bullet>a))"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns m) = val_Zp (f' \<bullet> a)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (1 + int n) - val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
using 11
[PROOF STATE]
proof (prove)
using this:
val_Zp (f' \<bullet> ns m) = val_Zp (f' \<bullet> a)
eint 2 * val_Zp (f' \<bullet> a) + 1 + eint (int n) - val_Zp (f' \<bullet> ns m) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)

goal (1 subgoal):
 1. eint 2 * val_Zp (f' \<bullet> a) + eint (1 + int n) - val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
by (smt eSuc_eint iadd_Suc iadd_Suc_right)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (f' \<bullet> a) + eint (1 + int n) - val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)

goal (1 subgoal):
 1. eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint 2 * val_Zp (f' \<bullet> a) + eint (1 + int n) - val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
have 14:"val_Zp (f\<bullet> (ns m)) - val_Zp (f'\<bullet>(ns m))
                                \<ge> 1 + int n +  val_Zp ((f'\<bullet>a))"
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (1 + int n) - val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)

goal (1 subgoal):
 1. eint (1 + int n) + val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
using eint_minus_comm[of "2*(val_Zp (f'\<bullet>a))" "1 + int n" "val_Zp ((f'\<bullet>a))"]
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) + eint (1 + int n) - val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
eint 2 * val_Zp (f' \<bullet> a) + eint (1 + int n) - val_Zp (f' \<bullet> a) = eint 2 * val_Zp (f' \<bullet> a) - val_Zp (f' \<bullet> a) + eint (1 + int n)

goal (1 subgoal):
 1. eint (1 + int n) + val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
by (simp add: Groups.add_ac(2))
[PROOF STATE]
proof (state)
this:
eint (1 + int n) + val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)

goal (1 subgoal):
 1. eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint (1 + int n) + val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eint (1 + int n) + val_Zp (f' \<bullet> a) \<le> val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)

goal (1 subgoal):
 1. eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
by (smt Suc_ile_eq add.right_neutral eint.distinct(2) f'a_nonneg_val ge_plus_pos_imp_gt order_less_le)
[PROOF STATE]
proof (state)
this:
eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)

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

goal (1 subgoal):
 1. eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eint (int n) < val_Zp (f \<bullet> ns m) - val_Zp (f' \<bullet> ns m)

goal (1 subgoal):
 1. eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
by (smt "0" Suc_ile_eq of_nat_Suc)
[PROOF STATE]
proof (state)
this:
eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
int (Suc n) + k0 + 1 \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>m. int (Suc n) + k0 + 1 \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)

goal (1 subgoal):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m. int (Suc n) + k0 + 1 \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>m. int (Suc n) + k0 + 1 \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)

goal (1 subgoal):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
using val_Zp_def val_Zp_dist_def
[PROOF STATE]
proof (prove)
using this:
\<forall>m. int (Suc n) + k0 + 1 \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp_dist (newton_step (ns m)) (ns m)
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)

goal (1 subgoal):
 1. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)
[PROOF STEP]
by (metis newton_seq.simps(2))
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int (Suc n)) \<le> val_Zp (ns (Suc m) \<ominus> ns m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. \<exists>k. \<forall>m. k \<le> int m \<longrightarrow> eint (int n) \<le> val_Zp (ns (Suc m) \<ominus> ns m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eventually_zero:
"f \<bullet> ns (k + m) = \<zero> \<Longrightarrow> f \<bullet> ns (k + Suc m) = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> ns (k + m) = \<zero> \<Longrightarrow> f \<bullet> ns (k + Suc m) = \<zero>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<bullet> ns (k + m) = \<zero> \<Longrightarrow> f \<bullet> ns (k + Suc m) = \<zero>
[PROOF STEP]
assume A: "f \<bullet> ns (k + m) = \<zero>"
[PROOF STATE]
proof (state)
this:
f \<bullet> ns (k + m) = \<zero>

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

goal (1 subgoal):
 1. f \<bullet> ns (k + m) = \<zero> \<Longrightarrow> f \<bullet> ns (k + Suc m) = \<zero>
[PROOF STEP]
have 1: "(divide (f \<bullet> ns (k + m)) (f' \<bullet> ns (k + m))) = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> ns (k + m)) (f' \<bullet> ns (k + m)) = \<zero>
[PROOF STEP]
by (simp add: A divide_def)
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns (k + m)) (f' \<bullet> ns (k + m)) = \<zero>

goal (1 subgoal):
 1. f \<bullet> ns (k + m) = \<zero> \<Longrightarrow> f \<bullet> ns (k + Suc m) = \<zero>
[PROOF STEP]
show "f \<bullet> ns (k + Suc m) = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> ns (k + Suc m) = \<zero>
[PROOF STEP]
using A 0 1
[PROOF STATE]
proof (prove)
using this:
f \<bullet> ns (k + m) = \<zero>
ns (k + Suc m) = ns (k + m) \<ominus> local.divide (f \<bullet> ns (k + m)) (f' \<bullet> ns (k + m))
local.divide (f \<bullet> ns (k + m)) (f' \<bullet> ns (k + m)) = \<zero>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma newton_seq_is_Zp_cauchy:
"is_Zp_cauchy ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_Zp_cauchy ns
[PROOF STEP]
proof(cases "\<forall>k. f\<bullet>(ns k) \<noteq>\<zero>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>k. f \<bullet> ns k \<noteq> \<zero> \<Longrightarrow> is_Zp_cauchy ns
 2. \<not> (\<forall>k. f \<bullet> ns k \<noteq> \<zero>) \<Longrightarrow> is_Zp_cauchy ns
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>k. f \<bullet> ns k \<noteq> \<zero>

goal (2 subgoals):
 1. \<forall>k. f \<bullet> ns k \<noteq> \<zero> \<Longrightarrow> is_Zp_cauchy ns
 2. \<not> (\<forall>k. f \<bullet> ns k \<noteq> \<zero>) \<Longrightarrow> is_Zp_cauchy ns
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>k. f \<bullet> ns k \<noteq> \<zero>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>k. f \<bullet> ns k \<noteq> \<zero>

goal (1 subgoal):
 1. is_Zp_cauchy ns
[PROOF STEP]
using newton_seq_is_Zp_cauchy_0
[PROOF STATE]
proof (prove)
using this:
\<forall>k. f \<bullet> ns k \<noteq> \<zero>
(\<And>k. f \<bullet> ns k \<noteq> \<zero>) \<Longrightarrow> is_Zp_cauchy ns

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

goal (1 subgoal):
 1. \<not> (\<forall>k. f \<bullet> ns k \<noteq> \<zero>) \<Longrightarrow> is_Zp_cauchy ns
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>k. f \<bullet> ns k \<noteq> \<zero>) \<Longrightarrow> is_Zp_cauchy ns
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>k. f \<bullet> ns k \<noteq> \<zero>)

goal (1 subgoal):
 1. \<not> (\<forall>k. f \<bullet> ns k \<noteq> \<zero>) \<Longrightarrow> is_Zp_cauchy ns
[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 False
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>k. f \<bullet> ns k \<noteq> \<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 (1 subgoal):
 1. \<not> (\<forall>k. f \<bullet> ns k \<noteq> \<zero>) \<Longrightarrow> is_Zp_cauchy ns
[PROOF STEP]
have 0: "\<And>m. (ns (m + k)) = (ns k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. ns (m + k) = ns k
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. ns (m + k) = ns k
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. ns (m + k) = ns k
[PROOF STEP]
show "(ns (m + k)) = (ns k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns (m + k) = ns k
[PROOF STEP]
proof(induction m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ns (0 + k) = ns k
 2. \<And>m. ns (m + k) = ns k \<Longrightarrow> ns (Suc m + k) = ns k
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

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

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

goal (1 subgoal):
 1. \<And>m. ns (m + k) = ns k \<Longrightarrow> ns (Suc m + k) = ns k
[PROOF STEP]
show "(ns (Suc m + k)) = (ns k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns (Suc m + k) = ns k
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns (Suc m + k) = ns k
[PROOF STEP]
have "f \<bullet> ns (m + k) = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> ns (m + k) = \<zero>
[PROOF STEP]
by (simp add: Suc.IH k_def)
[PROOF STATE]
proof (state)
this:
f \<bullet> ns (m + k) = \<zero>

goal (1 subgoal):
 1. ns (Suc m + k) = ns k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<bullet> ns (m + k) = \<zero>
[PROOF STEP]
have "divide ( f \<bullet> ns (m + k)) (f' \<bullet> ns (m + k)) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
f \<bullet> ns (m + k) = \<zero>

goal (1 subgoal):
 1. local.divide (f \<bullet> ns (m + k)) (f' \<bullet> ns (m + k)) = \<zero>
[PROOF STEP]
by (simp add: divide_def)
[PROOF STATE]
proof (state)
this:
local.divide (f \<bullet> ns (m + k)) (f' \<bullet> ns (m + k)) = \<zero>

goal (1 subgoal):
 1. ns (Suc m + k) = ns k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.divide (f \<bullet> ns (m + k)) (f' \<bullet> ns (m + k)) = \<zero>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.divide (f \<bullet> ns (m + k)) (f' \<bullet> ns (m + k)) = \<zero>

goal (1 subgoal):
 1. ns (Suc m + k) = ns k
[PROOF STEP]
using newton_step_def
[PROOF STATE]
proof (prove)
using this:
local.divide (f \<bullet> ns (m + k)) (f' \<bullet> ns (m + k)) = \<zero>
newton_step ?x = ?x \<ominus> local.divide (f \<bullet> ?x) (f' \<bullet> ?x)

goal (1 subgoal):
 1. ns (Suc m + k) = ns k
[PROOF STEP]
by (simp add: Suc.IH a_minus_def newton_seq_closed)
[PROOF STATE]
proof (state)
this:
ns (Suc m + k) = ns k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns (Suc m + k) = ns k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns (m + k) = ns k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns (?m2 + k) = ns k

goal (1 subgoal):
 1. \<not> (\<forall>k. f \<bullet> ns k \<noteq> \<zero>) \<Longrightarrow> is_Zp_cauchy ns
[PROOF STEP]
show "is_Zp_cauchy ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_Zp_cauchy ns
[PROOF STEP]
apply(rule is_Zp_cauchyI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ns \<in> carrier Zp\<^bsup>\<omega>\<^esup>
 2. \<And>n. \<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
apply (simp add: closed_seqs_memI newton_seq_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
show "\<And>n.\<And>n. \<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 n = ns n1 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 na = ns n1 na
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n na. \<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 na = ns n1 na
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n na. \<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 na = ns n1 na
[PROOF STEP]
show "\<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 n = ns n1 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
have "\<forall>n0 n1. k < n0 \<and> k < n1 \<longrightarrow> ns n0 n = ns n1 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n0 n1. k < n0 \<and> k < n1 \<longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n0 n1. \<lbrakk>k < n0; k < n1\<rbrakk> \<Longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n0 n1. \<lbrakk>k < n0; k < n1\<rbrakk> \<Longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
fix n0 n1
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n0 n1. \<lbrakk>k < n0; k < n1\<rbrakk> \<Longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
assume A0: "k < n0"
[PROOF STATE]
proof (state)
this:
k < n0

goal (1 subgoal):
 1. \<And>n0 n1. \<lbrakk>k < n0; k < n1\<rbrakk> \<Longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
assume A1: "k < n1"
[PROOF STATE]
proof (state)
this:
k < n1

goal (1 subgoal):
 1. \<And>n0 n1. \<lbrakk>k < n0; k < n1\<rbrakk> \<Longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
obtain m0 where m0_def: "n0 = k + m0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m0. n0 = k + m0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A0 less_imp_add_positive
[PROOF STATE]
proof (prove)
using this:
k < n0
?i < ?j \<Longrightarrow> \<exists>k>0. ?i + k = ?j

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

goal (1 subgoal):
 1. \<And>n0 n1. \<lbrakk>k < n0; k < n1\<rbrakk> \<Longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
obtain m1 where m1_def: "n1 = k + m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m1. n1 = k + m1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A1 less_imp_add_positive
[PROOF STATE]
proof (prove)
using this:
k < n1
?i < ?j \<Longrightarrow> \<exists>k>0. ?i + k = ?j

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

goal (1 subgoal):
 1. \<And>n0 n1. \<lbrakk>k < n0; k < n1\<rbrakk> \<Longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
show "ns n0 n = ns n1 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns n0 n = ns n1 n
[PROOF STEP]
using 0 m0_def m1_def
[PROOF STATE]
proof (prove)
using this:
ns (?m2 + k) = ns k
n0 = k + m0
n1 = k + m1

goal (1 subgoal):
 1. ns n0 n = ns n1 n
[PROOF STEP]
by (metis add.commute)
[PROOF STATE]
proof (state)
this:
ns n0 n = ns n1 n

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

goal (1 subgoal):
 1. \<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n0 n1. k < n0 \<and> k < n1 \<longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n0 n1. k < n0 \<and> k < n1 \<longrightarrow> ns n0 n = ns n1 n

goal (1 subgoal):
 1. \<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 n = ns n1 n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 n = ns n1 n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 n = ns n1 n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>N. \<forall>n0 n1. N < n0 \<and> N < n1 \<longrightarrow> ns n0 ?na2 = ns n1 ?na2

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

goal:
No subgoals!
[PROOF STEP]
qed