Theory Padic_Field_Polynomials

theory Padic_Field_Polynomials
  imports Padic_Fields

begin

(**************************************************************************************************)
(**************************************************************************************************)
section‹$p$-adic Univariate Polynomials and Hensel's Lemma›
(**************************************************************************************************)
(**************************************************************************************************)
type_synonym padic_field_poly = "nat ⇒ padic_number"

type_synonym padic_field_fun = "padic_number ⇒ padic_number"

(**************************************************************************************************)
(**************************************************************************************************)
subsection‹Gauss Norms of Polynomials›
(**************************************************************************************************)
(**************************************************************************************************)

text ‹
  The Gauss norm of a polynomial is defined to be the minimum valuation of a coefficient of that
  polynomial. This induces a valuation on the ring of polynomials, and in particular it satisfies
  the ultrametric inequality. In addition, the Gauss norm of a polynomial $f(x)$ gives a lower
  bound for the value $\text{val } (f(a))$ in terms of $\text{val }(a)$, for a point
  $a \in \mathbb{Q}_p$. We introduce Gauss norms here as a useful tool for stating and proving
  Hensel's Lemma for the field $\mathbb{Q}_p$. We are abusing terminology slightly in calling
  this the Gauss norm, rather than the Gauss valuation, but this is just to conform with our
  decision to work exclusively with the $p$-adic valuation and not discuss the equivalent
  real-valued $p$-adic norm. For a detailed treatment of Gauss norms one can see, for example
  cite‹"engler2005valued"›.
›
context padic_fields
begin

no_notation Zp.to_fun (infixl‹∙› 70)

abbreviation(input) Qp_x where
"Qp_x ≡ UP Qp"

definition gauss_norm where
"gauss_norm g = Min (val ` g ` {..degree g}) "

lemma gauss_normE:
  assumes "g ∈ carrier Qp_x"
  shows "gauss_norm g ≤ val (g k)"
  apply(cases "k ≤ degree g")
  unfolding gauss_norm_def
  using assms apply auto[1]
proof-
  assume "¬ k ≤ degree g"
  then have "g k = 𝟬⇘Qp⇙ "
    by (simp add: UPQ.deg_leE assms)
  then show "Min (val ` g ` {..deg Qp g}) ≤ val (g k)"
    by (simp add: local.val_zero)
qed

lemma gauss_norm_geqI:
  assumes "g ∈ carrier (UP Qp)"
  assumes "⋀n. val (g n) ≥ α"
  shows "gauss_norm g ≥ α"
  unfolding gauss_norm_def using assms
  by simp

lemma gauss_norm_eqI:
  assumes "g ∈ carrier (UP Qp)"
  assumes "⋀n. val (g n) ≥ α"
  assumes "val (g i) = α"
  shows "gauss_norm g = α"
proof-
  have 0: "gauss_norm g ≤ α"
    using assms gauss_normE gauss_norm_def by fastforce
  have 1: "gauss_norm g ≥ α"
    using assms gauss_norm_geqI by auto
  show ?thesis using 0 1 by auto
qed

lemma nonzero_poly_nonzero_coeff:
  assumes "g ∈ carrier Qp_x"
  assumes "g ≠ 𝟬⇘Qp_x⇙"
  shows "∃k. k ≤degree g ∧ g k ≠𝟬⇘Qp⇙"
proof(rule ccontr)
  assume "¬ (∃k≤degree g. g k ≠ 𝟬⇘Qp⇙)"
  then have 0: "⋀k. g k = 𝟬⇘Qp⇙"
    by (meson UPQ.deg_leE assms(1) not_le_imp_less)
  then show False
    using assms  UPQ.cfs_zero by blast
qed

lemma gauss_norm_prop:
  assumes "g ∈ carrier Qp_x"
  assumes "g ≠ 𝟬⇘Qp_x⇙"
  shows "gauss_norm g ≠ ∞"
proof-
  obtain k where k_def: "k ≤degree g ∧ g k ≠𝟬⇘Qp⇙"
    using assms nonzero_poly_nonzero_coeff
    by blast
  then have 0: "gauss_norm g ≤ val (g k)"
    using assms(1) gauss_normE by blast
  have "g k ∈ carrier Qp"
    using UPQ.cfs_closed assms(1) by blast
  hence "val (g k) < ∞"
    using k_def assms
    by (metis eint_ord_code(3) eint_ord_simps(4) val_ineq)
  then show ?thesis
    using 0 not_le by fastforce
qed

lemma gauss_norm_coeff_norm:
  "∃n ≤ degree g. (gauss_norm g) = val (g n)"
proof-
  have "finite (val ` g ` {..deg Qp g})"
    by blast
  hence "∃x ∈ (val ` g ` {..deg Qp g}). gauss_norm g = x"
  unfolding gauss_norm_def
  by auto
  thus ?thesis unfolding gauss_norm_def
    by blast
qed

lemma gauss_norm_smult_cfs:
  assumes "g ∈ carrier Qp_x"
  assumes "a ∈ carrier Qp"
  assumes "gauss_norm g = val (g k)"
  shows "gauss_norm (a ⊙⇘Qp_x⇙ g) = val a + val (g k)"
proof-
  obtain l where l_def: "gauss_norm (a ⊙⇘Qp_x⇙ g) =  val ((a ⊙⇘Qp_x⇙ g) l)"
    using gauss_norm_coeff_norm
    by blast
  then have "gauss_norm (a ⊙⇘Qp_x⇙ g) =  val (a ⊗⇘Qp⇙ (g l))"
    using assms
    by simp
  then have "gauss_norm (a ⊙⇘Qp_x⇙ g) =  val a + val (g l)"
    by (simp add: UPQ.cfs_closed assms(1) assms(2) val_mult)
  then have 0: "gauss_norm (a ⊙⇘Qp_x⇙ g) ≤ val a +val (g k)"
    using assms  gauss_normE[of g l]
    by (metis UPQ.UP_smult_closed UPQ.cfs_closed UPQ.cfs_smult gauss_normE val_mult)
  have "val a + val (g k) = val ((a ⊙⇘Qp_x⇙ g) k)"
    by (simp add: UPQ.cfs_closed assms(1) assms(2) val_mult)
  then have "gauss_norm (a ⊙⇘Qp_x⇙ g) ≥ val a + val (g k)"
    by (metis ‹gauss_norm (a ⊙⇘UP Qp⇙ g) = val a + val (g l)› add_left_mono assms(1) assms(3) gauss_normE)
  then show ?thesis
    using 0  by auto
qed

lemma gauss_norm_smult:
  assumes "g ∈ carrier Qp_x"
  assumes "a ∈ carrier Qp"
  shows "gauss_norm (a ⊙⇘Qp_x⇙ g) = val a + gauss_norm g"
  using gauss_norm_smult_cfs[of g a] gauss_norm_coeff_norm[of g] assms
  by metis

lemma gauss_norm_ultrametric:
  assumes "g ∈ carrier Qp_x"
  assumes "h ∈ carrier Qp_x"
  shows "gauss_norm (g ⊕⇘Qp_x⇙ h) ≥ min (gauss_norm g) (gauss_norm h)"
proof-
  obtain k where "gauss_norm (g ⊕⇘Qp_x⇙ h) = val ((g ⊕⇘Qp_x⇙ h) k)"
    using gauss_norm_coeff_norm
    by blast
  then have 0: "gauss_norm (g ⊕⇘Qp_x⇙ h) = val (g k ⊕⇘Qp⇙ h k)"
    by (simp add: assms(1) assms(2))
  have "min (val (g k)) (val (h k))≥ min (gauss_norm g) (gauss_norm h)"
    using gauss_normE[of g k] gauss_normE[of h k]  assms(1) assms(2) min.mono
    by blast
  then show ?thesis
    using 0 val_ultrametric[of "g k" "h k"] assms(1) assms(2) dual_order.trans
    by (metis (no_types, lifting) UPQ.cfs_closed)
qed

lemma gauss_norm_a_inv:
  assumes "f ∈ carrier (UP Qp)"
  shows "gauss_norm (⊖⇘UP Qp⇙f) = gauss_norm f"
proof-
  have 0: "⋀n. ((⊖⇘UP Qp⇙f) n) = ⊖ (f n)"
    using assms by simp
  have 1: "⋀n. val ((⊖⇘UP Qp⇙f) n) = val (f n)"
    using 0 assms UPQ.UP_car_memE(1) val_minus by presburger
  obtain i where i_def: "gauss_norm f = val (f i)"
    using assms gauss_norm_coeff_norm by blast
  have 2: "⋀k. val ((⊖⇘UP Qp⇙f) k) ≥ val (f i)"
    unfolding 1
    using i_def assms gauss_normE by fastforce
  show ?thesis
    apply(rule gauss_norm_eqI[of _ _ i])
      apply (simp add: assms; fail)
    unfolding 1 using assms gauss_normE apply blast
    unfolding i_def by blast
qed

lemma gauss_norm_ultrametric':
  assumes "f ∈ carrier (UP Qp)"
  assumes "g ∈ carrier (UP Qp)"
  shows "gauss_norm (f ⊖⇘UP Qp⇙ g) ≥ min (gauss_norm f) (gauss_norm g)"
  unfolding a_minus_def
  using assms gauss_norm_a_inv[of g] gauss_norm_ultrametric
  by (metis UPQ.UP_a_inv_closed)

lemma gauss_norm_finsum:
  assumes "f ∈ A → carrier Qp_x"
  assumes "finite A"
  assumes "A ≠ {}"
  shows " gauss_norm (⨁⇘Qp_x⇙i∈A. f i) ≥ Min (gauss_norm ` (f`A))"
proof-
  obtain k where k_def: "val ((⨁⇘Qp_x⇙i∈A. f i) k) = gauss_norm (⨁⇘Qp_x⇙i∈A. f i)"
    by (metis gauss_norm_coeff_norm)
  then have 0: "val (⨁⇘Qp⇙i∈A. f i k) ≥ Min (val ` (λ i. f i k) ` A)"
    using finsum_val_ultrametric[of "λ i. f i k" A] assms
    by (simp add: ‹⟦(λi. f i k) ∈ A → carrier Qp; finite A; A ≠ {}⟧ ⟹ Min (val ` (λi. f i k) ` A) ≤ val (⨁i∈A. f i k)› Pi_iff UPQ.cfs_closed)
  have "(⋀a. a ∈ A ⟹ (val ∘ (λi. f i k)) a ≥ gauss_norm (f a))"
    using gauss_normE assms
    by (metis (no_types, lifting) Pi_split_insert_domain Set.set_insert comp_apply)
  then have "Min (val ` (λ i. f i k) ` A) ≥ Min ((λ i. gauss_norm (f  i)) ` A)"
    using Min_mono'[of A]
    by (simp add: assms(2) image_comp)
  then have 1: "Min (val ` (λ i. f i k) ` A) ≥ Min (gauss_norm ` f ` A)"
    by (metis image_image)
  have "f ∈ A → carrier (UP Qp) ⟶ ((⨁⇘Qp_x⇙i∈A. f i) ∈ carrier Qp_x ∧ ((⨁⇘Qp_x⇙i∈A. f i) k) = (⨁⇘Qp⇙i∈A. f i k)) "
    apply(rule finite.induct[of A])
      apply (simp add: assms(2); fail)
     apply (metis (no_types, lifting) Pi_I Qp.add.finprod_one_eqI UPQ.P.finsum_closed UPQ.P.finsum_empty UPQ.cfs_zero empty_iff)
  proof-
    fix a A assume A: "finite A" "f ∈ A → carrier (UP Qp) ⟶ ( finsum (UP Qp) f A ∈ carrier (UP Qp) ∧ finsum (UP Qp) f A k = (⨁i∈A. f i k)) "
    show " f ∈ insert a A → carrier (UP Qp) ⟶  finsum (UP Qp) f (insert a A) ∈ carrier (UP Qp) ∧ finsum (UP Qp) f (insert a A) k = (⨁i∈insert a A. f i k)"
      apply(cases "a ∈ A")
      using A
      apply (simp add: insert_absorb; fail)
    proof assume B: "a ∉ A" " f ∈ insert a A → carrier (UP Qp)"
      then have f_a: "f a ∈ carrier (UP Qp)"
        by blast
      have f_A: "f ∈ A → carrier (UP Qp)"
        using B by blast
      have "finsum (UP Qp) f (insert a A) = f a ⊕⇘UP Qp⇙finsum (UP Qp) f A"
        using assms A B f_a f_A  finsum_insert by simp
      then have 0: "finsum (UP Qp) f (insert a A) k = f a k ⊕⇘Qp⇙ (finsum (UP Qp) f A) k"
        using f_a f_A A B
        by simp
      have " ( λ a. f a k) ∈ A → carrier Qp"
      proof fix a assume "a ∈ A"
        then have "f a ∈ carrier (UP Qp)"
          using f_A by blast
        then show "f a k ∈ carrier Qp"
          using A cfs_closed by blast
      qed
      then have 0: "finsum (UP Qp) f (insert a A) k = (⨁i∈insert a A. f i k)"
        using A B Qp.finsum_insert[of A a "λ a. f a k"]
        by (simp add: UPQ.cfs_closed)
      thus " finsum (UP Qp) f (insert a A) ∈ carrier (UP Qp) ∧ finsum (UP Qp) f (insert a A) k = (⨁i∈insert a A. f i k)"
        using B(2) UPQ.P.finsum_closed by blast
    qed
  qed
  then have "(⨁⇘Qp_x⇙i∈A. f i) ∈ carrier Qp_x ∧ ((⨁⇘Qp_x⇙i∈A. f i) k) = (⨁⇘Qp⇙i∈A. f i k)"
    using assms by blast
  hence 3: "gauss_norm (⨁⇘Qp_x⇙i∈A. f i) ≥ Min (val ` (λ i. f i k) ` A)"
    using 0  k_def by auto
  thus ?thesis
    using 1 le_trans by auto
qed

lemma gauss_norm_monom:
  assumes "a ∈ carrier Qp"
  shows "gauss_norm (monom Qp_x a n) = val a"
proof-
  have "val ((monom Qp_x a n) n) ≥ gauss_norm (monom Qp_x a n)"
    using assms gauss_normE[of "monom Qp_x a n" n] UPQ.monom_closed
    by blast
  then show ?thesis
    using gauss_norm_coeff_norm[of "monom Qp_x a n"] assms val_ineq UPQ.cfs_monom by fastforce
qed

lemma val_val_ring_prod:
  assumes "a ∈ 𝒪p"
  assumes "b ∈ carrier Qp"
  shows "val (a ⊗⇘Qp⇙ b) ≥ val b"
proof-
  have 0: "val (a ⊗⇘Qp⇙ b) = val a + val b"
    using assms val_ring_memE[of a] val_mult
    by blast
  have 1: " val a ≥ 0"
    using assms
    by (simp add: val_ring_memE)
  then show ?thesis
    using assms 0
    by simp
qed

lemma val_val_ring_prod':
  assumes "a ∈ 𝒪p"
  assumes "b ∈ carrier Qp"
  shows "val (b ⊗⇘Qp⇙ a) ≥ val b"
  using val_val_ring_prod[of a b]
  by (simp add: Qp.m_comm val_ring_memE assms(1) assms(2))

lemma val_ring_nat_pow_closed:
  assumes "a ∈ 𝒪p"
  shows "(a[^](n::nat)) ∈ 𝒪p"
  apply(induction n)
  apply auto[1]
  using Qp.inv_one Zp_mem apply blast
  by (metis Qp.nat_pow_Suc Qp.nat_pow_closed val_ring_memE assms image_eqI inc_of_prod to_Zp_closed to_Zp_inc to_Zp_mult)

lemma val_ringI:
  assumes "a ∈ carrier Qp"
  assumes "val a ≥0"
  shows " a ∈ 𝒪p"
  apply(rule val_ring_val_criterion)
  using assms by auto

notation UPQ.to_fun (infixl‹∙› 70)

lemma val_gauss_norm_eval:
  assumes "g ∈ carrier Qp_x"
  assumes "a ∈ 𝒪p"
  shows "val (g ∙ a) ≥ gauss_norm g"
proof-
  have 0: "g∙a = (⨁⇘Qp⇙i∈{..degree g}. (g i)⊗⇘Qp⇙ (a[^]i))"
    using val_ring_memE assms to_fun_formula[of g a] by auto

  have 1: "(λi. g i ⊗⇘Qp⇙ (a[^]i)) ∈ {..degree g} → carrier Qp"
     using assms
    by (meson Pi_I val_ring_memE cfs_closed monom_term_car)
  then have 2: "val (g∙a) ≥ Min (val ` (λ i. ((g i)⊗⇘Qp⇙ (a[^]i))) ` {..degree g})"
    using 0 finsum_val_ultrametric[of "λ i. ((g i)⊗⇘Qp⇙ (a[^]i))" "{..degree g}" ]
    by (metis finite_atMost not_empty_eq_Iic_eq_empty)
  have 3: "⋀ i. val ((g i)⊗⇘Qp⇙ (a[^]i)) = val (g i) + val (a[^]i)"
    using assms val_mult
    by (simp add: val_ring_memE UPQ.cfs_closed)
  have 4: "⋀ i. val ((g i)⊗⇘Qp⇙ (a[^]i)) ≥ val (g i)"
  proof-
    fix i
    show "val ((g i)⊗⇘Qp⇙ (a[^]i)) ≥ val (g i)"
      using val_val_ring_prod'[of "a[^]i" "g i" ]
        assms(1) assms(2) val_ring_nat_pow_closed cfs_closed
      by simp
  qed
  have "Min (val ` (λi. g i ⊗⇘Qp⇙ (a[^]i)) ` {..degree g}) ≥ Min ((λi. val (g i)) ` {..degree g})"
    using Min_mono'[of "{..degree g}" "λi. val (g i)" "λi. val (g i ⊗⇘Qp⇙ (a[^]i))" ] 4 2
    by (metis finite_atMost image_image)
  then have "Min (val ` (λi. g i ⊗⇘Qp⇙ (a[^]i)) ` {..degree g}) ≥ Min (val ` g ` {..degree g})"
    by (metis  image_image)
  then have  "val (g∙a) ≥ Min (val ` g ` {..degree g})"
    using 2
    by (meson atMost_iff atMost_subset_iff in_mono)
  then show ?thesis
    by (simp add: ‹val (g∙a) ≥ Min (val ` g ` {..degree g})› gauss_norm_def)
qed

lemma positive_gauss_norm_eval:
  assumes "g ∈ carrier Qp_x"
  assumes "gauss_norm g ≥ 0"
  assumes "a ∈ 𝒪p"
  shows "(g∙a) ∈ 𝒪p"
  apply(rule val_ring_val_criterion[of "g∙a"])
  using assms val_ring_memE
  using UPQ.to_fun_closed apply blast
  using assms val_gauss_norm_eval[of g a] by auto

lemma positive_gauss_norm_valuation_ring_coeffs:
  assumes "g ∈ carrier Qp_x"
  assumes "gauss_norm g ≥ 0"
  shows "g n ∈ 𝒪p"
  apply(rule val_ringI)
  using cfs_closed assms(1) apply blast
  using gauss_normE[of g n] assms by auto

lemma val_ring_cfs_imp_nonneg_gauss_norm:
  assumes "g ∈ carrier (UP Qp)"
  assumes "⋀n. g n ∈ 𝒪p"
  shows "gauss_norm g ≥ 0"
  by(rule gauss_norm_geqI, rule assms, rule val_ring_memE, rule assms)

lemma val_of_add_pow:
  assumes "a ∈ carrier Qp"
  shows "val ([(n::nat)]⋅a) ≥ val a"
proof-
  have 0: "[(n::nat)]⋅a = ([n]⋅𝟭)⊗a"
    using assms Qp.add_pow_ldistr Qp.cring_simprules(12) Qp.one_closed by presburger
  have 1: "val ([(n::nat)]⋅a) = val ([n]⋅𝟭) + val a"
    unfolding 0 by(rule val_mult, simp, rule assms)
  show ?thesis unfolding 1 using assms
    by (simp add: val_of_nat_inc)
qed

lemma gauss_norm_pderiv:
  assumes "g ∈ carrier (UP Qp)"
  shows "gauss_norm g ≤ gauss_norm (pderiv g)"
  apply(rule gauss_norm_geqI)
  using UPQ.pderiv_closed assms apply blast
  using gauss_normE pderiv_cfs val_of_add_pow
  by (smt UPQ.cfs_closed assms dual_order.trans)

(**************************************************************************************************)
(**************************************************************************************************)
subsection‹Mapping Polynomials with Value Ring Coefficients to Polynomials over $\mathbb{Z}_p$›
(**************************************************************************************************)
(**************************************************************************************************)

definition to_Zp_poly where
"to_Zp_poly g = (λn. to_Zp (g n))"

lemma to_Zp_poly_closed:
  assumes "g ∈ carrier Qp_x"
  assumes "gauss_norm g ≥ 0"
  shows "to_Zp_poly g ∈ carrier (UP Zp)"
proof-
  have  "to_Zp_poly g ∈ up Zp"
    apply(rule mem_upI)
   unfolding to_Zp_poly_def
   using cfs_closed[of g ] assms(1) to_Zp_closed[of ]  apply blast
  proof-
    have "∃n. bound 𝟬⇘Qp⇙ n g"
     using UPQ.deg_leE assms(1) by auto
    then obtain n where n_def: " bound 𝟬⇘Qp⇙ n g"
      by blast
    then have " bound 𝟬⇘Zp⇙ n (λn. to_Zp (g n))"
      unfolding bound_def
      by (simp add: to_Zp_zero)
    then show "∃n. bound 𝟬⇘Zp⇙ n (λn. to_Zp (g n))"
      by blast
  qed
  then show ?thesis using UP_def[of Zp]
    by simp
qed

definition poly_inc where
"poly_inc g = (λn::nat. ι (g n))"

lemma poly_inc_closed:
  assumes "g ∈ carrier (UP Zp)"
  shows "poly_inc g ∈ carrier Qp_x"
proof-
  have "poly_inc g ∈ up Qp"
  proof(rule mem_upI)
    show "⋀n. poly_inc g n ∈ carrier Qp"
    proof- fix n
      have "g n ∈ carrier Zp"
        using assms UP_def
        by (simp add: UP_def mem_upD)
      then show "poly_inc g n ∈ carrier Qp"
        using assms poly_inc_def[of g] inc_def[of "g n" ] inc_closed
        by force
    qed
    show "∃n. bound 𝟬⇘Qp⇙ n (poly_inc g)"
    proof-
      obtain n where n_def: " bound 𝟬⇘Zp⇙ n g"
        using assms  bound_def[of "𝟬⇘Zp⇙" _ g]Zp.cring_axioms UP_cring.deg_leE[of Zp g]
        unfolding UP_cring_def
        by metis
      then have " bound 𝟬⇘Qp⇙ n (poly_inc g)"
        unfolding poly_inc_def bound_def
        by (metis Qp.nat_inc_zero Zp.nat_inc_zero inc_of_nat)
      then show ?thesis by blast
    qed
  qed
  then show ?thesis
    by (simp add: ‹poly_inc g ∈ up Qp› UP_def)
qed

lemma poly_inc_inverse_right:
  assumes "g ∈ carrier (UP Zp)"
  shows "to_Zp_poly (poly_inc g) = g"
proof-
  have 0: "⋀n. g n ∈ carrier Zp"
    by (simp add: Zp.cfs_closed assms)
  show ?thesis
    unfolding to_Zp_poly_def poly_inc_def
  proof
    fix n
    show "to_Zp (ι (g n)) = g n"
      using 0 inc_to_Zp
      by auto
  qed
qed

lemma poly_inc_inverse_left:
  assumes "g ∈ carrier Qp_x"
  assumes "gauss_norm g ≥0"
  shows "poly_inc (to_Zp_poly g) = g"
proof
  fix x
  show "poly_inc (to_Zp_poly g) x = g x"
    using assms unfolding poly_inc_def to_Zp_poly_def
    by (simp add: positive_gauss_norm_valuation_ring_coeffs to_Zp_inc)
qed

lemma poly_inc_plus:
  assumes "f ∈ carrier (UP Zp)"
  assumes "g ∈ carrier (UP Zp)"
  shows "poly_inc (f ⊕⇘UP Zp⇙ g) = poly_inc f ⊕⇘UP Qp⇙ poly_inc g"
proof
  fix n
  have 0: "poly_inc (f ⊕⇘UP Zp⇙ g) n = ι (f n ⊕⇘Zp⇙ g n)"
    unfolding poly_inc_def using assms by auto
  have 1: "(poly_inc f ⊕⇘UP Qp⇙ poly_inc g) n = poly_inc f n ⊕ poly_inc g n"
    by(rule cfs_add, rule poly_inc_closed, rule assms, rule poly_inc_closed, rule assms)
  show "poly_inc (f ⊕⇘UP Zp⇙ g) n = (poly_inc f ⊕⇘UP Qp⇙ poly_inc g) n"
    unfolding 0 1 unfolding poly_inc_def
    apply(rule inc_of_sum)
    using assms apply (simp add: Zp.cfs_closed; fail)
        using assms by (simp add: Zp.cfs_closed)
qed

lemma poly_inc_monom:
  assumes "a ∈ carrier Zp"
  shows "poly_inc (monom (UP Zp) a m) = monom (UP Qp) (ι a) m"
proof fix n
  show "poly_inc (monom (UP Zp) a m) n = monom (UP Qp) (ι a) m n"
    apply(cases "m = n")
    using assms cfs_monom[of "ι a"] Zp.cfs_monom[of a] unfolding poly_inc_def
     apply (simp add: inc_closed; fail)
    using assms cfs_monom[of "ι a"] Zp.cfs_monom[of a] unfolding poly_inc_def
    by (metis Qp.nat_mult_zero Zp_nat_inc_zero inc_closed inc_of_nat)
qed

lemma poly_inc_times:
  assumes "f ∈ carrier (UP Zp)"
  assumes "g ∈ carrier (UP Zp)"
  shows "poly_inc (f ⊗⇘UP Zp⇙ g) = poly_inc f ⊗⇘UP Qp⇙ poly_inc g"
  apply(rule UP_ring.poly_induct3[of Zp])
  apply (simp add: Zp.is_UP_ring; fail)
  using assms apply blast
proof-
  fix p q
  assume A: "q ∈ carrier (UP Zp)"  "p ∈ carrier (UP Zp)"
            "poly_inc (f ⊗⇘UP Zp⇙ p) = poly_inc f ⊗⇘UP Qp⇙ poly_inc p"
            "poly_inc (f ⊗⇘UP Zp⇙ q) = poly_inc f ⊗⇘UP Qp⇙ poly_inc q"
  have 0: "(f ⊗⇘UP Zp⇙ (p ⊕⇘UP Zp⇙ q)) = (f ⊗⇘UP Zp⇙ p) ⊕⇘UP Zp⇙ (f ⊗⇘UP Zp⇙ q)"
    using assms(1) A
    by (simp add: Zp.P.r_distr)
  have 1: "poly_inc (p ⊕⇘UP Zp⇙ q) = poly_inc p ⊕⇘UP Qp⇙ poly_inc q"
    by(rule poly_inc_plus, rule A, rule A)
  show "poly_inc (f ⊗⇘UP Zp⇙ (p ⊕⇘UP Zp⇙ q)) = poly_inc f ⊗⇘UP Qp⇙ poly_inc (p ⊕⇘UP Zp⇙ q)"
    unfolding 0 1 using A poly_inc_closed poly_inc_plus
    by (simp add: UPQ.P.r_distr assms(1))
next
  fix a fix n::nat
  assume A: "a ∈ carrier Zp"
  show "poly_inc (f ⊗⇘UP Zp⇙ monom (UP Zp) a n) =
           poly_inc f ⊗⇘UP Qp⇙ poly_inc (monom (UP Zp) a n)"
  proof
    fix m
    show "poly_inc (f ⊗⇘UP Zp⇙ monom (UP Zp) a n) m =
         (poly_inc f ⊗⇘UP Qp⇙ poly_inc (monom (UP Zp) a n)) m"
    proof(cases "m < n")
      case True
      have T0: "(f ⊗⇘UP Zp⇙ monom (UP Zp) a n) m = 𝟬⇘Zp⇙"
        using True Zp.cfs_monom_mult[of f a m n] A assms
        by blast
      have T1: "poly_inc (monom (UP Zp) a n) =  (monom (UP Qp) (ι a) n)"
        by(rule poly_inc_monom , rule A)
      show ?thesis
        unfolding T0 T1 using True
        by (metis A Qp_def T0 UPQ.cfs_monom_mult Zp_def assms(1) inc_closed padic_fields.to_Zp_zero padic_fields_axioms poly_inc_closed poly_inc_def to_Zp_inc zero_in_val_ring)
    next
      case False
      then have F0: "m ≥ n"
        using False by simp
      have F1: "(f ⊗⇘UP Zp⇙ monom (UP Zp) a n) m = a ⊗⇘Zp⇙ f (m - n)"
        using Zp.cfs_monom_mult_l' F0 A assms by simp
      have F2: "poly_inc (monom (UP Zp) a n)  = monom (UP Qp) (ι a) n "
        by(rule poly_inc_monom, rule A)
      have F3: "(poly_inc f ⊗⇘UP Qp⇙ poly_inc (monom (UP Zp) a n)) m
                = (ι a) ⊗ (poly_inc f (m -n))"
        using UPQ.cfs_monom_mult_l' F0 A assms poly_inc_closed
        by (simp add: F2 inc_closed)
      show ?thesis
        unfolding F3 unfolding poly_inc_def F1
        apply(rule inc_of_prod, rule A)
        using assms Zp.cfs_closed by blast
    qed
  qed
qed

lemma poly_inc_one:
"poly_inc (𝟭⇘UP Zp⇙) = 𝟭⇘UP Qp⇙"
apply(rule ext)
  unfolding poly_inc_def
  using inc_of_one inc_of_zero
  by simp

lemma poly_inc_zero:
"poly_inc (𝟬⇘UP Zp⇙) = 𝟬⇘UP Qp⇙"
apply(rule ext)
  unfolding poly_inc_def
  using inc_of_one inc_of_zero
  by simp

lemma poly_inc_hom:
"poly_inc ∈ ring_hom (UP Zp) (UP Qp)"
  apply(rule ring_hom_memI)
     apply(rule poly_inc_closed, blast)
    apply(rule poly_inc_times, blast, blast)
   apply(rule poly_inc_plus, blast, blast)
  by(rule poly_inc_one)

lemma poly_inc_as_poly_lift_hom:
  assumes "f ∈ carrier (UP Zp)"
  shows "poly_inc f = poly_lift_hom Zp Qp ι f"
  apply(rule ext)
  unfolding poly_inc_def
  using Zp.poly_lift_hom_cf[of Qp ι f] assms UPQ.R_cring local.inc_is_hom
  by blast

lemma poly_inc_eval:
  assumes "g ∈ carrier (UP Zp)"
  assumes "a ∈ carrier Zp"
  shows "to_function Qp (poly_inc g) (ι a) = ι (to_function Zp g a)"
proof-
  have 0: "poly_inc g = poly_lift_hom Zp Qp ι g"
    using assms poly_inc_as_poly_lift_hom[of g] by blast
  have 1: "to_function Qp (poly_lift_hom Zp Qp ι g) (ι a) = ι (to_function Zp g a)"
    using Zp.poly_lift_hom_eval[of Qp ι g a] assms inc_is_hom
    unfolding to_fun_def Zp.to_fun_def
    using UPQ.R_cring by blast
  show ?thesis unfolding 0 1
    by blast
qed

lemma val_ring_poly_eval:
  assumes "f ∈ carrier (UP Qp)"
  assumes "⋀ i. f i ∈ 𝒪p"
  shows "⋀x. x ∈ 𝒪p ⟹ f ∙ x ∈ 𝒪p"
  apply(rule positive_gauss_norm_eval, rule assms)
  apply(rule val_ring_cfs_imp_nonneg_gauss_norm)
  using assms by auto

lemma Zp_res_of_pow:
  assumes "a ∈ carrier Zp"
  assumes "b ∈ carrier Zp"
  assumes "a n = b n"
  shows "(a[^]⇘Zp⇙(k::nat)) n = (b[^]⇘Zp⇙(k::nat)) n"
  apply(induction k)
  using assms Group.nat_pow_0 to_Zp_one apply metis
  using Zp.geometric_series_id[of a b] Zp_residue_mult_zero(1) assms(1) assms(2) assms(3)
    pow_closed res_diff_zero_fact'' res_diff_zero_fact(1) by metis

lemma to_Zp_nat_pow:
  assumes "a ∈ 𝒪p"
  shows "to_Zp (a[^](n::nat)) = (to_Zp a)[^]⇘Zp⇙(n::nat)"
  apply(induction n)
  using assms Group.nat_pow_0 to_Zp_one apply metis
  using assms to_Zp_mult[of a] Qp.m_comm Qp.nat_pow_Suc val_ring_memE pow_suc to_Zp_closed val_ring_nat_pow_closed
  by metis

lemma  to_Zp_res_of_pow:
  assumes "a ∈ 𝒪p"
  assumes "b ∈ 𝒪p"
  assumes "to_Zp a n = to_Zp b n"
  shows "to_Zp (a[^](k::nat)) n = to_Zp (b[^](k::nat)) n"
  using assms val_ring_memE Zp_res_of_pow to_Zp_closed to_Zp_nat_pow by presburger

lemma poly_eval_cong:
  assumes "g ∈ carrier (UP Qp)"
  assumes "⋀i. g i ∈ 𝒪p"
  assumes "a ∈ 𝒪p"
  assumes "b ∈ 𝒪p"
  assumes "to_Zp a k = to_Zp b k"
  shows "to_Zp (g ∙ a) k = to_Zp (g ∙ b) k"
proof-
  have "(∀i. g i ∈ 𝒪p) ⟶ to_Zp (g ∙ a) k = to_Zp (g ∙ b) k"
  proof(rule UPQ.poly_induct[of g])
    show " g ∈ carrier (UP Qp)"
      using assms by blast
    show "⋀p. p ∈ carrier (UP Qp) ⟹ deg Qp p = 0 ⟹ (∀i. p i ∈ 𝒪p) ⟶ to_Zp (p ∙ a) k = to_Zp (p ∙ b) k"
    proof fix p assume A: "p ∈ carrier (UP Qp)" "deg Qp p = 0" "∀i. p i ∈ 𝒪p"
      obtain c where c_def: "c ∈ carrier Qp ∧ p = up_ring.monom (UP Qp) c 0"
        using A
        by (metis UPQ.zcf_degree_zero UPQ.cfs_closed UPQ.trms_of_deg_leq_0 UPQ.trms_of_deg_leq_degree_f)
      have p_eq: "p = up_ring.monom (UP Qp) c 0"
        using c_def by blast
      have p_cfs: "p 0 = c"
        unfolding p_eq using c_def UP_ring.cfs_monom[of Qp c 0 0] UPQ.P_is_UP_ring by presburger
      have c_closed: "c ∈ 𝒪p"
        using p_cfs A(3) by blast
      have 0: "(p ∙ a) = c"
        unfolding p_eq using c_def assms by (meson UPQ.to_fun_const val_ring_memE(2))
      have 1: "(p ∙ b) = c"
        unfolding p_eq using c_def assms UPQ.to_fun_const val_ring_memE(2) by presburger
      show " to_Zp (p ∙ a) k = to_Zp (p ∙ b) k"
        unfolding 0 1 by blast
    qed
    show "⋀p. (⋀q. q ∈ carrier (UP Qp) ⟹ deg Qp q < deg Qp p ⟹ (∀i. q i ∈ 𝒪p) ⟶ to_Zp (q ∙ a) k = to_Zp (q ∙ b) k) ⟹
         p ∈ carrier (UP Qp) ⟹ 0 < deg Qp p ⟹ (∀i. p i ∈ 𝒪p) ⟶ to_Zp (p ∙ a) k = to_Zp (p ∙ b) k"
    proof
      fix p assume A: "(⋀q. q ∈ carrier (UP Qp) ⟹ deg Qp q < deg Qp p ⟹ (∀i. q i ∈ 𝒪p) ⟶ to_Zp (q ∙ a) k = to_Zp (q ∙ b) k)"
                      "p ∈ carrier (UP Qp)" "0 < deg Qp p " " ∀i. p i ∈ 𝒪p"
      obtain q where q_def: "q ∈ carrier (UP Qp) ∧ deg Qp q < deg Qp p ∧ p = UPQ.ltrm p ⊕⇘UP Qp⇙q"
        by (metis A(2) A(3) UPQ.ltrm_closed UPQ.ltrm_decomp UPQ.UP_a_comm)
      have 0: "⋀i.  p i = q i ⊕ UPQ.ltrm p i"
        using q_def A
        by (metis Qp.a_ac(2) UPQ.ltrm_closed UPQ.UP_car_memE(1) UPQ.cfs_add)
      have 1: "∀i. q i ∈ 𝒪p"
      proof fix i
        show "q i ∈ 𝒪p"
          apply(cases "i < deg Qp p")
          using 0[of i] A(4) A(2) q_def
          using UPQ.ltrm_closed UPQ.P.a_ac(2) UPQ.trunc_cfs UPQ.trunc_closed UPQ.trunc_simps(1)
           apply (metis Qp.r_zero UPQ.ltrm_cfs UPQ.cfs_closed UPQ.deg_leE)
          using q_def
          by (metis (no_types, opaque_lifting) A(2) A(4) UPQ.P.add.m_closed UPQ.coeff_of_sum_diff_degree0 UPQ.deg_leE UPQ.equal_deg_sum UPQ.equal_deg_sum' ‹⋀thesis. (⋀q. q ∈ carrier (UP Qp) ∧ deg Qp q < deg Qp p ∧ p = up_ring.monom (UP Qp) (p (deg Qp p)) (deg Qp p) ⊕⇘UP Qp⇙ q ⟹ thesis) ⟹ thesis› lessI linorder_neqE_nat)
      qed
      have 2: "UPQ.lcf p ∈ 𝒪p"
        using A(4) by blast
      have 3: "UPQ.ltrm p ∙ a = UPQ.lcf p ⊗ a[^] deg Qp p"
        apply(rule UP_cring.to_fun_monom) unfolding UP_cring_def
          apply (simp add: UPQ.R_cring)
         apply (simp add: A(2) UPQ.cfs_closed)
        using assms(3) val_ring_memE(2) by blast
      have 4: "UPQ.ltrm p ∙ b = UPQ.lcf p ⊗ b[^] deg Qp p"
        apply(rule UP_cring.to_fun_monom) unfolding UP_cring_def
          apply (simp add: UPQ.R_cring)
         apply (simp add: A(2) UPQ.cfs_closed)
        using assms val_ring_memE(2) by blast
      have p_eq: "p = q ⊕⇘UP Qp⇙ UPQ.ltrm p"
        using q_def by (metis A(2) UPQ.ltrm_closed UPQ.UP_a_comm)
      have 5: "p ∙ a = q ∙ a ⊕  UPQ.lcf p ⊗ a[^] deg Qp p"
        using assms val_ring_memE(2) p_eq q_def UPQ.to_fun_plus[of q "UPQ.ltrm p" a]
        by (metis "3" A(2) UPQ.ltrm_closed UPQ.to_fun_plus)
      have 6: "p ∙ b = q ∙ b ⊕  UPQ.lcf p ⊗ b[^] deg Qp p"
        using assms val_ring_memE(2) p_eq q_def UPQ.to_fun_plus[of q "UPQ.ltrm p" a]
        by (metis "4" A(2) UPQ.ltrm_closed UPQ.to_fun_plus)
      have 7: "UPQ.lcf p ⊗ b[^] deg Qp p ∈ 𝒪p"
        apply(rule val_ring_times_closed)
        using "2" apply linarith
        by(rule val_ring_nat_pow_closed, rule assms)
      have 8: "UPQ.lcf p ⊗ a[^] deg Qp p ∈ 𝒪p"
        apply(rule val_ring_times_closed)
        using "2" apply linarith
        by(rule val_ring_nat_pow_closed, rule assms)
      have 9: "q ∙ a ∈ 𝒪p"
        using q_def 1 assms(3) val_ring_poly_eval by blast
      have 10: "q ∙ b ∈ 𝒪p"
        using q_def 1 assms(4) val_ring_poly_eval by blast
      have 11: "to_Zp (p ∙ a) = to_Zp (q ∙ a) ⊕⇘Zp⇙ to_Zp (UPQ.ltrm p ∙ a)"
        using 5 8 9 to_Zp_add 3 by presburger
      have 12: "to_Zp (p ∙ b) = to_Zp (q ∙ b) ⊕⇘Zp⇙ to_Zp (UPQ.ltrm p ∙ b)"
        using 6 10 7 to_Zp_add 4  by presburger
      have 13: "to_Zp (p ∙ a) k = to_Zp (q ∙ a) k ⊕⇘Zp_res_ring k⇙ to_Zp (UPQ.ltrm p ∙ a) k"
        unfolding 11 using residue_of_sum by blast
      have 14: "to_Zp (p ∙ b) k = to_Zp (q ∙ b) k ⊕⇘Zp_res_ring k⇙ to_Zp (UPQ.ltrm p ∙ b) k"
        unfolding 12 using residue_of_sum by blast
      have 15: "to_Zp (UPQ.ltrm p ∙ a) k = to_Zp (UPQ.ltrm p ∙ b) k"
      proof(cases "k = 0")
        case True
        have T0: "to_Zp (UPQ.ltrm p ∙ a) ∈ carrier Zp"
          unfolding 3 using 8  to_Zp_closed val_ring_memE(2) by blast
        have T1: "to_Zp (UPQ.ltrm p ∙ b) ∈ carrier Zp"
          unfolding 4 using 7 to_Zp_closed val_ring_memE(2) by blast
        show ?thesis unfolding True using T0 T1 padic_integers.p_res_ring_0
          by (metis p_res_ring_0' residues_closed)
      next
        case False
        have k_pos: "k > 0"
          using False by presburger
        have 150: "to_Zp (p (deg Qp p) ⊗ a [^] deg Qp p) = to_Zp (p (deg Qp p)) ⊗⇘Zp⇙ to_Zp( a [^] deg Qp p)"
         apply(rule to_Zp_mult)
          using "2" apply blast
         by(rule val_ring_nat_pow_closed, rule assms)
        have 151: "to_Zp (p (deg Qp p) ⊗ b [^] deg Qp p) = to_Zp (p (deg Qp p)) ⊗⇘Zp⇙ to_Zp( b [^] deg Qp p)"
         apply(rule to_Zp_mult)
          using "2" apply blast
         by(rule val_ring_nat_pow_closed, rule assms)
       have 152: "to_Zp (p (deg Qp p) ⊗ a [^] deg Qp p) k = to_Zp (p (deg Qp p)) k ⊗⇘Zp_res_ring k⇙ to_Zp( a [^] deg Qp p) k"
         unfolding 150 using residue_of_prod by blast
       have 153: "to_Zp (p (deg Qp p) ⊗ b [^] deg Qp p) k = to_Zp (p (deg Qp p)) k ⊗⇘Zp_res_ring k⇙ to_Zp( b [^] deg Qp p) k"
         unfolding 151 using residue_of_prod by blast
       have 154: "to_Zp( a [^] deg Qp p) k = to_Zp a k [^]⇘Zp_res_ring k⇙ deg Qp p"
       proof-
       have 01: "⋀m::nat. to_Zp (a[^]m) k = to_Zp a k [^]⇘Zp_res_ring k⇙ m"
       proof-
         fix m::nat show "to_Zp (a [^] m) k = to_Zp a k [^]⇘Zp_res_ring k⇙ m"
       proof-
         have 00: "to_Zp (a[^]m) = to_Zp a [^]⇘Zp⇙ m"
         using assms to_Zp_nat_pow[of a "m"] by blast
       have 01: "to_Zp a ∈ carrier Zp"
         using assms to_Zp_closed val_ring_memE(2) by blast
       have 02: "to_Zp a k ∈ carrier (Zp_res_ring k)"
         using 01 residues_closed by blast
       have 03: "cring (Zp_res_ring k)"
         using k_pos padic_integers.R_cring padic_integers_axioms by blast
       have 01: "(to_Zp a [^]⇘Zp⇙ m) k = (to_Zp a) k [^]⇘Zp_res_ring k⇙ m"
         apply(induction m)
         using 01 02 apply (metis Group.nat_pow_0 k_pos residue_of_one(1))
         using residue_of_prod[of "to_Zp a [^]⇘Zp⇙ m" "to_Zp a" k] 01 02 03
       proof -
         fix ma :: nat
         assume "(to_Zp a [^]⇘Zp⇙ ma) k = to_Zp a k [^]⇘Zp_res_ring k⇙ ma"
         then show "(to_Zp a [^]⇘Zp⇙ Suc ma) k = to_Zp a k [^]⇘Zp_res_ring k⇙ Suc ma"
           by (metis (no_types) Group.nat_pow_Suc residue_of_prod)
       qed
       show ?thesis unfolding 00 01 by blast
       qed
       qed
       thus ?thesis by blast
       qed
       have 155: "to_Zp( b [^] deg Qp p) k = to_Zp b k [^]⇘Zp_res_ring k⇙ deg Qp p"
         using assms by (metis "154" to_Zp_res_of_pow)
       show ?thesis
         unfolding 3 4 152 153 154 155 assms by blast
     qed
     show "to_Zp (p ∙ a) k = to_Zp (p ∙ b) k"
       unfolding 13 14 15 using A 1 q_def by presburger
   qed
  qed
  thus ?thesis using assms by blast
qed

lemma to_Zp_poly_eval:
  assumes "g ∈ carrier Qp_x"
  assumes "gauss_norm g ≥ 0"
  assumes "a ∈ 𝒪p"
  shows "to_Zp (to_function Qp g a) = to_function Zp (to_Zp_poly g) (to_Zp a)"
proof-
  obtain h where h_def: "h = to_Zp_poly g"
    by blast
  obtain b where b_def: "b = to_Zp a"
    by blast
  have h_poly_inc: "poly_inc h = g"
    unfolding h_def using assms
    by (simp add: poly_inc_inverse_left)
  have b_inc: "ι b = a"
    unfolding b_def using assms
    by (simp add: to_Zp_inc)
  have h_closed: "h ∈ carrier (UP Zp)"
    unfolding h_def using assms
    by (simp add: to_Zp_poly_closed)
  have b_closed: "b ∈ carrier Zp"
    unfolding b_def using assms
    by (simp add: to_Zp_closed val_ring_memE)
  have 0: "to_function Qp (poly_inc h) (ι b) = ι (to_function Zp h b)"
    apply(rule poly_inc_eval)
    using h_def assms apply (simp add: to_Zp_poly_closed; fail)
    unfolding b_def using assms
    by (simp add: to_Zp_closed val_ring_memE)
  have 1: "to_Zp (to_function Qp (poly_inc h) (ι b)) = to_function Zp h b"
    unfolding 0
    using h_closed b_closed Zp.to_fun_closed Zp.to_fun_def inc_to_Zp by auto
  show ?thesis
    using 1 unfolding h_poly_inc b_inc
    unfolding h_def b_def by blast
qed

lemma poly_eval_equal_val:
  assumes "g ∈ carrier (UP Qp)"
  assumes "⋀x. g x ∈ 𝒪p"
  assumes "a ∈ 𝒪p"
  assumes "b ∈ 𝒪p"
  assumes "val (g ∙ a) < eint n"
  assumes "to_Zp a n = to_Zp b n"
  shows "val (g ∙ b) = val (g ∙ a)"
proof-
  have "(∀x. g x ∈ 𝒪p) ⟶ to_Zp (g ∙ b) n = to_Zp (g ∙ a) n"
  proof(rule poly_induct[of g])
    show "g ∈ carrier (UP Qp)"
      by (simp add: assms(1))
    show "⋀p. p ∈ carrier (UP Qp) ⟹ deg Qp p = 0 ⟹ (∀x. p x ∈ 𝒪p) ⟶ to_Zp (p ∙ b) n = to_Zp (p ∙ a) n"
    proof fix p assume A: "p ∈ carrier (UP Qp)" " deg Qp p = 0 " "∀x. p x ∈ 𝒪p "
      show "to_Zp (p ∙ b) n = to_Zp (p ∙ a) n"
        using A  by (metis val_ring_memE UPQ.to_fun_ctrm UPQ.trms_of_deg_leq_0 UPQ.trms_of_deg_leq_degree_f assms(3) assms(4))
    qed
    show "⋀p. (⋀q. q ∈ carrier (UP Qp) ⟹ deg Qp q < deg Qp p ⟹ (∀x. q x ∈ 𝒪p) ⟶ to_Zp (q ∙ b) n = to_Zp (q ∙ a) n) ⟹
         p ∈ carrier (UP Qp) ⟹ 0 < deg Qp p ⟹ (∀x. p x ∈ 𝒪p) ⟶ to_Zp (p ∙ b) n = to_Zp (p ∙ a) n"
    proof fix p assume IH: "(⋀q. q ∈ carrier (UP Qp) ⟹ deg Qp q < deg Qp p ⟹ (∀x. q x ∈ 𝒪p) ⟶ to_Zp (q ∙ b) n = to_Zp (q ∙ a) n)"
      assume A: "p ∈ carrier (UP Qp)" "0 < deg Qp p" "∀x. p x ∈ 𝒪p"
      show "to_Zp (p ∙ b) n = to_Zp (p ∙ a) n"
      proof-
        obtain q where q_def: "q ∈ carrier (UP Qp) ∧ deg Qp q < deg Qp p ∧
                      p = q ⊕⇘UP Qp⇙ ltrm p"
          using A  by (meson UPQ.ltrm_decomp)
        have p_eq: "p = q ⊕⇘UP Qp⇙ ltrm p"
          using q_def by blast
        have "∀x. q x ∈ 𝒪p" proof fix x
          have px: "p x = (q ⊕⇘UP Qp⇙ ltrm p) x"
            using p_eq by simp
          show "q x ∈ 𝒪p"
          proof(cases "x ≤ deg Qp q")
            case True
            then have "p x = q x"
              unfolding px using q_def A
              by (smt UPQ.ltrm_closed UPQ.P.add.right_cancel UPQ.coeff_of_sum_diff_degree0 UPQ.deg_ltrm UPQ.trunc_cfs UPQ.trunc_closed UPQ.trunc_simps(1) less_eq_Suc_le nat_neq_iff not_less_eq_eq)
            then show ?thesis using A
              by blast
          next
            case False
            then show ?thesis
              using q_def UPQ.deg_eqI eq_imp_le nat_le_linear zero_in_val_ring
              by (metis (no_types, lifting) UPQ.coeff_simp UPQ.deg_belowI)
          qed
        qed
        then have 0: " to_Zp (q ∙ b) n = to_Zp (q ∙ a) n"
          using IH q_def by blast
        have 1: "to_Zp (ltrm p ∙ b) n = to_Zp (ltrm p ∙ a) n"
        proof-
          have 10: "(ltrm p ∙ b) = (p (deg Qp p)) ⊗ b[^] (deg Qp p)"
            using assms A  by (meson val_ring_memE UPQ.to_fun_monom)
          have 11: "(ltrm p ∙ a) = (p (deg Qp p)) ⊗ a[^] (deg Qp p)"
            using assms A by (meson val_ring_memE UPQ.to_fun_monom)
          have 12: "to_Zp (b[^] (deg Qp p)) n = to_Zp (a[^] (deg Qp p)) n"
            using to_Zp_res_of_pow assms by metis
          have 13: "p (deg Qp p) ∈ 𝒪p"
            using A(3) by blast
          have 14: "b[^] (deg Qp p) ∈ 𝒪p"
            using assms(4) val_ring_nat_pow_closed by blast
          have 15: "a[^] (deg Qp p) ∈ 𝒪p"
            using assms(3) val_ring_nat_pow_closed by blast
          have 16: "(ltrm p ∙ b) ∈ 𝒪p"
            by (simp add: "10" "13" "14" val_ring_times_closed)
          have 17: "to_Zp (ltrm p ∙ b) n = to_Zp (p (deg Qp p)) n ⊗⇘Zp_res_ring n⇙ to_Zp (b[^] (deg Qp p)) n"
            using 10 13 14 15 16 assms residue_of_prod to_Zp_mult by presburger
          have 18: "(ltrm p ∙ a) ∈ 𝒪p"
            by (simp add: "11" "15" A(3) val_ring_times_closed)
          have 19: "to_Zp (ltrm p ∙ a) n = to_Zp (p (deg Qp p)) n ⊗⇘Zp_res_ring n⇙ to_Zp (a[^] (deg Qp p)) n"
            using 10 13 14 15 16 17 18 assms residue_of_prod to_Zp_mult 11  by presburger
          show ?thesis using 12 17 19 by presburger
        qed
        have 2: "p (deg Qp p) ∈ 𝒪p"
          using A(3) by blast
        have 3: "(ltrm p ∙ b) ∈ 𝒪p"
          using 2 assms
          by (metis A(1) Qp_def val_ring_memE val_ring_memE UPQ.ltrm_closed Zp_def ι_def
              gauss_norm_monom padic_fields.positive_gauss_norm_eval padic_fields_axioms)
        have 4: "(ltrm p ∙ a) ∈ 𝒪p"
          using 2 assms
          by (metis A(1) Qp_def val_ring_memE val_ring_memE UPQ.ltrm_closed Zp_def ι_def
              gauss_norm_monom padic_fields.positive_gauss_norm_eval padic_fields_axioms)
        have 5: "(q ∙ b) ∈ 𝒪p"
          using  ‹∀x. q x ∈ 𝒪p› assms(4) q_def
          by (metis gauss_norm_coeff_norm positive_gauss_norm_eval val_ring_memE(1))
        have 6: "(q ∙ a) ∈ 𝒪p"
          using  ‹∀x. q x ∈ 𝒪p› assms(3) q_def
          by (metis gauss_norm_coeff_norm positive_gauss_norm_eval val_ring_memE(1))
        have 7: "to_Zp (p ∙ b) = to_Zp (ltrm p ∙ b)  ⊕⇘Zp⇙ to_Zp (q ∙ b)"
          using 5 3 q_def by (metis (no_types, lifting) A(1) val_ring_memE UPQ.ltrm_closed UPQ.to_fun_plus add_comm assms(4) to_Zp_add)
        have 8: "to_Zp (p ∙ a) = to_Zp (ltrm p ∙ a)  ⊕⇘Zp⇙ to_Zp (q ∙ a)"
          using 4 6 q_def by (metis (no_types, lifting) A(1) val_ring_memE UPQ.ltrm_closed UPQ.to_fun_plus add_comm assms(3) to_Zp_add)
        have 9: "to_Zp (p ∙ b) ∈ carrier Zp"
          using A assms by (meson val_ring_memE UPQ.to_fun_closed to_Zp_closed)
        have 10: "to_Zp (p ∙ a) ∈ carrier Zp"
          using A assms val_ring_memE UPQ.to_fun_closed to_Zp_closed by presburger
        have 11: "to_Zp (p ∙ b) n = to_Zp (ltrm p ∙ b) n  ⊕⇘Zp_res_ring n⇙ to_Zp (q ∙ b) n"
          using 7 9 5 3 residue_of_sum by presburger
        have 12: "to_Zp (p ∙ a) n = to_Zp (ltrm p ∙ a) n ⊕⇘Zp_res_ring n⇙ to_Zp (q ∙ a) n"
          using 8 6 4 residue_of_sum by presburger
        show ?thesis using 0 11 12 q_def assms
          using "1" by presburger
      qed
    qed
  qed
  have "(∀x. g x ∈ 𝒪p) "
    using assms by blast
  hence 0: "to_Zp (g ∙ b) n = to_Zp (g ∙ a) n"
    using ‹(∀x. g x ∈ 𝒪p) ⟶ to_Zp (g ∙ b) n = to_Zp (g ∙ a) n› by blast
  have 1: "g ∙ a ∈ 𝒪p"
    using  assms(1) assms(2) assms(3)
    by (metis gauss_norm_coeff_norm positive_gauss_norm_eval val_ring_memE(1))
  have 2: "g ∙ b ∈ 𝒪p"
    using  assms(1) assms(2) assms(4)
    by (metis gauss_norm_coeff_norm positive_gauss_norm_eval val_ring_memE(1))
  have 3: "val (g ∙ b) < eint n"
  proof-
    have P0: "to_Zp (g ∙ a) ∈ carrier Zp"
      using 1 val_ring_memE to_Zp_closed by blast
    have P1: "to_Zp (g ∙ b) ∈ carrier Zp"
      using 2 val_ring_memE to_Zp_closed by blast
    have P2: "val_Zp (to_Zp (g ∙ a)) < n"
      using 1 assms to_Zp_val by presburger
    have P3: "to_Zp (g ∙ a) ≠ 𝟬⇘Zp⇙"
      using P2 P0 unfolding val_Zp_def     by (metis P2 infinity_ilessE val_Zp_def)
    have P4: "(to_Zp (g ∙ a)) n ≠ 0"
      using 1 P2 P3 above_ord_nonzero[of "to_Zp (g ∙ a)" n]
      by (metis P0 eint.inject less_eintE val_ord_Zp)
    then have "to_Zp (g ∙ b) n ≠ 0"
      using 0 by linarith
    then have "val_Zp (to_Zp (g ∙ b)) < n"
      using P1 P0
      by (smt below_val_Zp_zero eint_ile eint_ord_simps(1) eint_ord_simps(2) nonzero_imp_ex_nonzero_res residue_of_zero(2) zero_below_val_Zp)
    then show ?thesis using 2
      by (metis to_Zp_val)
  qed
  thus ?thesis using 0 1 2 assms val_ring_equal_res_imp_equal_val[of "g ∙ b" "g ∙ a" n] by blast
qed

lemma to_Zp_poly_monom:
  assumes "a ∈ 𝒪p"
  shows "to_Zp_poly (monom (UP Qp) a n) = monom (UP Zp) (to_Zp a) n"
  unfolding to_Zp_poly_def
  apply(rule ext)
  using assms cfs_monom[of a n] Zp.cfs_monom[of "to_Zp a" n]
  by (simp add: to_Zp_closed to_Zp_zero val_ring_memE(2))

lemma to_Zp_poly_add:
  assumes "f ∈ carrier (UP Qp)"
  assumes "gauss_norm f ≥ 0"
  assumes "g ∈ carrier (UP Qp)"
  assumes "gauss_norm g ≥ 0"
  shows "to_Zp_poly (f ⊕⇘UP Qp⇙ g) = to_Zp_poly f ⊕⇘UP Zp⇙ to_Zp_poly g"
proof-
  obtain F where F_def: "F = to_Zp_poly f"
    by blast
  obtain G where G_def: "G = to_Zp_poly g"
    by blast
  have F_closed: "F ∈ carrier (UP Zp)"
    unfolding F_def using assms
    by (simp add: to_Zp_poly_closed)
  have G_closed: "G ∈ carrier (UP Zp)"
    unfolding G_def using assms
    by (simp add: to_Zp_poly_closed)
  have F_inc: "poly_inc F = f"
    using assms unfolding F_def
    using poly_inc_inverse_left by blast
  have G_inc: "poly_inc G = g"
    using assms unfolding G_def
    by (simp add: poly_inc_inverse_left)
  have 0: "poly_inc (F ⊕⇘UP Zp⇙ G) = poly_inc F ⊕⇘UP Qp⇙ poly_inc G"
    using F_closed G_closed
    by (simp add: poly_inc_plus)
  have 1: "to_Zp_poly (poly_inc (F ⊕⇘UP Zp⇙ G)) = F ⊕⇘UP Zp⇙ G"
    using G_closed F_closed
    by (simp add: poly_inc_inverse_right)
  show ?thesis
    using  1 unfolding F_inc G_inc 0 unfolding F_def G_def
    by blast
qed

lemma to_Zp_poly_zero:
"to_Zp_poly (𝟬⇘UP Qp⇙) = 𝟬⇘UP Zp⇙"
  unfolding to_Zp_poly_def
  apply(rule ext)
  by (simp add: to_Zp_zero)

lemma to_Zp_poly_one:
"to_Zp_poly (𝟭⇘UP Qp⇙) = 𝟭⇘UP Zp⇙"
  unfolding to_Zp_poly_def
  apply(rule ext)
  by (metis Zp.UP_one_closed poly_inc_inverse_right poly_inc_one to_Zp_poly_def)

lemma val_ring_add_pow:
  assumes "a ∈ carrier Qp"
  assumes "val a ≥ 0"
  shows "val ([(n::nat)]⋅a) ≥ 0"
proof-
  have 0: "[(n::nat)]⋅a = ([n]⋅𝟭)⊗a"
    using assms Qp.add_pow_ldistr Qp.cring_simprules(12) Qp.one_closed by presburger
  show ?thesis unfolding 0 using assms
    by (meson Qp.nat_inc_closed val_ring_memE val_of_nat_inc val_ringI val_ring_times_closed)
qed

lemma to_Zp_poly_pderiv:
  assumes "g ∈ carrier (UP Qp)"
  assumes "gauss_norm g ≥ 0"
  shows "to_Zp_poly (pderiv g) = Zp.pderiv (to_Zp_poly g)"
proof-
  have 0: "gauss_norm g ≥ 0 ⟶ to_Zp_poly (pderiv g) = Zp.pderiv (to_Zp_poly g)"
  proof(rule poly_induct, rule assms, rule)
    fix p
    assume A: " p ∈ carrier (UP Qp)"
         "deg Qp p = 0"
         "0 ≤ gauss_norm p"
    obtain a where a_def: "a ∈ 𝒪p ∧ p = monom (UP Qp) a 0"
      using A
      by (metis UPQ.ltrm_deg_0 positive_gauss_norm_valuation_ring_coeffs)
    have p_eq: "p = monom (UP Qp) a 0"
      using a_def by blast
    have 0: "to_Zp_poly p = monom (UP Zp) (to_Zp a) 0"
      unfolding p_eq
      apply(rule to_Zp_poly_monom)
      using a_def by blast
    have 1: "UPQ.pderiv (monom (UP Qp) a 0) = 𝟬⇘UP Qp⇙"
      using A(1) A(2) UPQ.pderiv_deg_0 p_eq by blast
    have 2: "Zp.pderiv (monom (UP Zp) (to_Zp a) 0) = 𝟬⇘UP Zp⇙"
      apply(rule Zp.pderiv_deg_0)
       apply(rule Zp.monom_closed, rule to_Zp_closed)
      using a_def
       apply (simp add: val_ring_memE(2); fail)
      apply(cases "to_Zp a = 𝟬⇘Zp⇙")
      apply (simp; fail)
      apply(rule Zp.deg_monom, blast)
      using a_def
      by (simp add: to_Zp_closed val_ring_memE(2))
    show "to_Zp_poly (UPQ.pderiv p) = Zp.pderiv (to_Zp_poly p)"
      unfolding 0 unfolding p_eq
      unfolding 1 2 to_Zp_poly_zero by blast
  next
    fix p
    assume A: "⋀q. q ∈ carrier (UP Qp) ⟹
              deg Qp q < deg Qp p ⟹
              0 ≤ gauss_norm q ⟶
              to_Zp_poly (UPQ.pderiv q) = Zp.pderiv (to_Zp_poly q)"
              "p ∈ carrier (UP Qp)"
              " 0 < deg Qp p"
    show "0 ≤ gauss_norm p ⟶ to_Zp_poly (UPQ.pderiv p) = Zp.pderiv (to_Zp_poly p)"
    proof
      assume B: "0 ≤ gauss_norm p"
      obtain q where q_def: "q = trunc p"
        by blast
      have p_eq: "p = q ⊕⇘UP Qp⇙ ltrm p"
        by (simp add: A(2) UPQ.trunc_simps(1) q_def)
      have q_gauss_norm:    "gauss_norm q ≥ 0"
        unfolding q_def
        apply(rule gauss_norm_geqI)
        using A apply (simp add: UPQ.trunc_closed; fail)
        using trunc_cfs[of p] A gauss_normE
      proof -
        fix n :: nat
        have f1: "𝟬 = q (deg Qp p)"
          by (simp add: UPQ.deg_leE UPQ.trunc_closed UPQ.trunc_degree ‹0 < deg Qp p› ‹p ∈ carrier (UP Qp)› q_def)
        have "∀n. 0 ≤ val (p n)"
          by (meson B ‹p ∈ carrier (UP Qp)› eint_ord_trans gauss_normE)
        then show "0 ≤ val (Cring_Poly.truncate Qp p n)"
          using f1 by (metis (no_types) Qp.nat_mult_zero UPQ.ltrm_closed UPQ.coeff_of_sum_diff_degree0 UPQ.deg_ltrm UPQ.trunc_closed ‹⋀n. ⟦p ∈ carrier (UP Qp); n < deg Qp p⟧ ⟹ Cring_Poly.truncate Qp p n = p n› ‹p ∈ carrier (UP Qp)› nat_neq_iff p_eq q_def val_of_nat_inc)
      qed
      have 0: "to_Zp_poly (UPQ.pderiv q) = Zp.pderiv (to_Zp_poly q)"
        using A q_def q_gauss_norm
        by (simp add: UPQ.trunc_closed UPQ.trunc_degree)
      have 1: "UPQ.pderiv (monom (UP Qp) (p (deg Qp p)) (deg Qp p)) =
               monom (UP Qp) ([deg Qp p] ⋅ p (deg Qp p)) (deg Qp p - 1)"
        apply(rule pderiv_monom)
        using A by (simp add: UPQ.UP_car_memE(1))
      have 2: "Zp.pderiv (monom (UP Zp) (to_Zp (p (deg Qp p))) (deg Qp p)) =
    monom (UP Zp) ([deg Qp p] ⋅⇘Zp⇙ to_Zp ( p (deg Qp p))) (deg Qp p - 1)"
        using A  Zp.pderiv_monom[of "to_Zp ( p (deg Qp p))" "deg Qp p"]
        by (simp add: UPQ.lcf_closed to_Zp_closed)
      have 3: "to_Zp_poly (UPQ.pderiv (monom (UP Qp) (p (deg Qp p)) (deg Qp p))) = monom (UP Zp) (to_Zp ([deg Qp p] ⋅ p (deg Qp p))) (deg Qp p - 1)"
        unfolding 1 apply(rule to_Zp_poly_monom)
        apply(rule val_ring_memI)
         apply (simp add: A(2) UPQ.UP_car_memE(1); fail)
        apply(rule val_ring_add_pow)
        using A
        apply (simp add: UPQ.lcf_closed; fail)
        using B A
        by (simp add: positive_gauss_norm_valuation_ring_coeffs val_ring_memE(1))
      have 4: "to_Zp_poly (ltrm p) = monom (UP Zp) (to_Zp (p (deg Qp p))) (deg Qp p)"
        apply(rule to_Zp_poly_monom) using A
        by (simp add: B positive_gauss_norm_valuation_ring_coeffs)
      have 5: "to_Zp_poly (UPQ.pderiv (ltrm p)) = Zp.pderiv (to_Zp_poly (ltrm p))"
        unfolding 3 4 2
        by (simp add: A(2) B positive_gauss_norm_valuation_ring_coeffs to_Zp_nat_add_pow)
      have 6: "pderiv p = pderiv q ⊕⇘UP Qp⇙ pderiv (ltrm p)"
        using p_eq
        by (metis A(2) UPQ.ltrm_closed UPQ.pderiv_add UPQ.trunc_closed p_eq q_def)
      have 7: "to_Zp_poly p = to_Zp_poly q ⊕⇘UP Zp⇙ to_Zp_poly (ltrm p)"
        using p_eq
        by (metis (no_types, lifting) A(2) B UPQ.ltrm_closed UPQ.cfs_closed UPQ.trunc_closed gauss_norm_monom positive_gauss_norm_valuation_ring_coeffs q_def q_gauss_norm to_Zp_poly_add val_ring_memE(1))
      have 8: "to_Zp_poly  (pderiv p) =
                to_Zp_poly (UPQ.pderiv q) ⊕⇘UP Zp⇙
                 to_Zp_poly (UPQ.pderiv (monom (UP Qp) (p (deg Qp p)) (deg Qp p)))"
        unfolding 6 apply(rule to_Zp_poly_add)
           apply (simp add: A(2) UPQ.pderiv_closed UPQ.trunc_closed q_def; fail)
          apply (metis A(2) UPQ.cfs_closed UPQ.pderiv_cfs UPQ.trunc_closed gauss_norm_coeff_norm positive_gauss_norm_valuation_ring_coeffs q_def q_gauss_norm val_ring_add_pow val_ring_memE(1))
         apply (simp add: A(2) UPQ.UP_car_memE(1) UPQ.pderiv_closed; fail)
        apply(rule eint_ord_trans[of _ "gauss_norm (monom (UP Qp) (p (deg Qp p)) (deg Qp p))"])
        apply (simp add: A(2) B UPQ.cfs_closed gauss_norm_monom positive_gauss_norm_valuation_ring_coeffs val_ring_memE(1); fail)
        apply(rule gauss_norm_pderiv)
        using A(2) UPQ.ltrm_closed by blast
      have 9: "Zp.pderiv  (to_Zp_poly p) =  Zp.pderiv (to_Zp_poly q) ⊕⇘UP Zp⇙
         Zp.pderiv (to_Zp_poly (monom (UP Qp) (p (deg Qp p)) (deg Qp p)))"
          unfolding 7 apply(rule Zp.pderiv_add)
           apply(rule to_Zp_poly_closed)
            apply (simp add: A(2) UPQ.trunc_closed q_def; fail)
           apply (simp add: q_gauss_norm; fail)
           apply(rule to_Zp_poly_closed)
           apply (simp add: A(2) UPQ.UP_car_memE(1); fail)
          by (simp add: A(2) B UPQ.cfs_closed gauss_norm_monom positive_gauss_norm_valuation_ring_coeffs val_ring_memE(1))
      show "to_Zp_poly (UPQ.pderiv p) = Zp.pderiv (to_Zp_poly p)"
          unfolding 9 8 5 0 by blast
    qed
  qed
  thus ?thesis using assms by blast
qed

lemma val_p_int_pow:
"val (𝔭[^]k) = eint (k)"
  by (simp add: ord_p_pow_int p_intpow_closed(2))

definition int_gauss_norm where
"int_gauss_norm g = (SOME n::int. eint n = gauss_norm g)"

lemma int_gauss_norm_eq:
  assumes "g ∈ carrier (UP Qp)"
  assumes "g ≠ 𝟬⇘UP Qp⇙"
  shows "eint (int_gauss_norm g) = gauss_norm g"
proof-
  have 0: "gauss_norm g < ∞"
    using assms by (simp add: gauss_norm_prop)
  then show ?thesis unfolding int_gauss_norm_def
    using assms
    by fastforce
qed

lemma int_gauss_norm_smult:
  assumes "g ∈ carrier (UP Qp)"
  assumes "g ≠ 𝟬⇘UP Qp⇙"
  assumes "a ∈ nonzero Qp"
  shows "int_gauss_norm (a ⊙⇘UP Qp⇙ g) = ord a + int_gauss_norm g"
  using gauss_norm_smult[of g a] int_gauss_norm_eq val_ord assms
  by (metis (no_types, opaque_lifting) Qp.nonzero_closed UPQ.UP_smult_closed UPQ.cfs_zero
      eint.distinct(2) eint.inject gauss_norm_coeff_norm local.val_zero plus_eint_simps(1))

definition normalize_poly where
"normalize_poly g = (if g = 𝟬⇘UP Qp⇙ then g else (𝔭[^](- int_gauss_norm g)) ⊙⇘Qp_x⇙ g)"

lemma normalize_poly_zero:
"normalize_poly 𝟬⇘UP Qp⇙ = 𝟬⇘UP Qp⇙"
  unfolding normalize_poly_def by simp

lemma normalize_poly_nonzero_eq:
  assumes "g ≠ 𝟬⇘UP Qp⇙"
  assumes "g ∈ carrier (UP Qp)"
  shows "normalize_poly g = (𝔭[^](- int_gauss_norm g)) ⊙⇘UP Qp⇙ g"
  using assms unfolding normalize_poly_def by simp

lemma int_gauss_norm_normalize_poly:
  assumes "g ≠ 𝟬⇘UP Qp⇙"
  assumes "g ∈ carrier (UP Qp)"
  shows "int_gauss_norm (normalize_poly g) = 0"
  using normalize_poly_nonzero_eq int_gauss_norm_smult assms
  by (simp add: ord_p_pow_int p_intpow_closed(2))

lemma normalize_poly_closed:
  assumes "g ∈ carrier (UP Qp)"
  shows "normalize_poly g ∈ carrier (UP Qp)"
  using assms unfolding normalize_poly_def
  by (simp add: p_intpow_closed(1))

lemma normalize_poly_nonzero:
  assumes "g ≠ 𝟬⇘UP Qp⇙"
  assumes "g ∈ carrier (UP Qp)"
  shows "normalize_poly g ≠ 𝟬⇘UP Qp⇙"
  using assms normalize_poly_nonzero_eq
  by (metis (no_types, lifting) UPQ.UP_smult_one UPQ.module_axioms UPQ.smult_r_null module.smult_assoc1 p_intpow_closed(1) p_intpow_inv')

lemma gauss_norm_normalize_poly:
  assumes "g ≠ 𝟬⇘UP Qp⇙"
  assumes "g ∈ carrier (UP Qp)"
  shows "gauss_norm (normalize_poly g) = 0"
proof-
  have 0: "eint (int_gauss_norm (normalize_poly g)) = gauss_norm (normalize_poly g)"
    by(rule int_gauss_norm_eq, rule normalize_poly_closed, rule assms,
          rule normalize_poly_nonzero, rule assms, rule assms)
  show ?thesis
    using 0 int_gauss_norm_normalize_poly assms
    by (simp add: zero_eint_def)
qed

lemma taylor_term_eval_eq:
  assumes "f ∈ carrier (UP Qp)"
  assumes "x ∈ carrier Qp"
  assumes "t ∈ carrier Qp"
  assumes "⋀j. i ≠ j ⟹ val (UPQ.taylor_term x f i ∙ t) < val (UPQ.taylor_term x f j ∙ t) "
  shows "val (f ∙ t) = val (UPQ.taylor_term x f i ∙ t)"
proof-
  have 0: "f = finsum (UP Qp) (UPQ.taylor_term x f) {..deg Qp f}"
    by(rule UPQ.taylor_term_sum[of f "deg Qp f" x], rule assms, blast, rule assms)
  show ?thesis
  proof(cases "i ∈ {..deg Qp f}")
    case True
    have T0: "finsum (UP Qp) (UPQ.taylor_term x f) {..deg Qp f} = UPQ.taylor_term x f i ⊕⇘UP Qp⇙ finsum (UP Qp) (UPQ.taylor_term x f) ({..deg Qp f} - {i})"
      apply(rule UPQ.P.finsum_remove[of "{..deg Qp f}" "UPQ.taylor_term x f" i])
      by(rule UPQ.taylor_term_closed, rule assms, rule assms, blast, rule True)
    have T1: "f = UPQ.taylor_term x f i ⊕⇘UP Qp⇙ finsum (UP Qp) (UPQ.taylor_term x f) ({..deg Qp f} - {i})"
      using 0 T0 by metis
    have T2: "finsum (UP Qp) (UPQ.taylor_term x f) ({..deg Qp f} - {i}) ∈ carrier (UP Qp)"
      apply(rule UPQ.P.finsum_closed)
      using UPQ.taylor_term_closed assms(1) assms(2) by blast
    have T3: "UPQ.taylor_term x f i ∈ carrier (UP Qp)"
      by(rule UPQ.taylor_term_closed, rule assms, rule assms )
    obtain g where g_def: "g = f"
      by blast
    have T4: "g = UPQ.taylor_term x f i ⊕⇘UP Qp⇙ finsum (UP Qp) (UPQ.taylor_term x f) ({..deg Qp f} - {i})"
      unfolding g_def by(rule T1)
    have g_closed: "g ∈ carrier (UP Qp)"
      unfolding g_def by(rule assms)
    have T5: "g ∙ t = UPQ.taylor_term x f i ∙ t ⊕ ( finsum (UP Qp) (UPQ.taylor_term x f) ({..deg Qp f} - {i})) ∙ t"
      unfolding T4 by(rule UPQ.to_fun_plus, rule T2, rule T3, rule assms)
    have T6: "( finsum (UP Qp) (UPQ.taylor_term x f) ({..deg Qp f} - {i})) ∙ t =
                ( finsum Qp (λi. UPQ.taylor_term x f i ∙ t) ({..deg Qp f} - {i}))"
      apply(rule UPQ.to_fun_finsum, blast)
      using assms UPQ.taylor_term_closed apply blast
      using assms by blast
    have T7: "⋀j. j ∈ {..deg Qp f} - {i} ⟹ val (UPQ.taylor_term x f j ∙ t) > val (UPQ.taylor_term x f i ∙ t)"
      using assms  by (metis Diff_iff singletonI)
    have T8: "val (( finsum (UP Qp) (UPQ.taylor_term x f) ({..deg Qp f} - {i})) ∙ t) > val (UPQ.taylor_term x f i ∙ t)"
      unfolding T6
      apply(rule finsum_val_ultrametric'')
      using UPQ.taylor_term_closed assms
      apply (metis (no_types, lifting) Pi_I UPQ.to_fun_closed)
        apply blast
      using assms T7 apply blast
      using assms(4)[of "Suc i"] using eint_ord_simps(4)
        assms(4) eint_ord_code(6)  g_def gr_implies_not_zero less_one by smt
    have T9: "val (g ∙ t) =  val (UPQ.taylor_term x f i ∙ t)"
      unfolding T5 using T8 T2 T3
      by (metis (no_types, lifting) Qp.add.m_comm UPQ.to_fun_closed assms(3) val_ultrametric_noteq)
    show ?thesis using T9 unfolding g_def by blast
  next
    case False
    have "i > deg Qp f"
      using False by simp
    hence "i > deg Qp (UPQ.taylor x f)"
      using assms UPQ.taylor_deg by presburger
    hence F0: "UPQ.taylor x f i = 𝟬"
      using assms UPQ.taylor_closed UPQ.deg_leE by blast
    have F1: "(UPQ.taylor_term x f i ∙ t) = 𝟬"
      using UPQ.to_fun_taylor_term[of f t x i]
      unfolding F0
      using assms Qp.cring_simprules(2) Qp.cring_simprules(4) Qp.integral_iff Qp.nat_pow_closed by presburger
    show ?thesis
      using assms(4)[of "Suc i"] unfolding F1
      by (metis eint_ord_code(6) local.val_zero n_not_Suc_n)
  qed
qed


(**************************************************************************************************)
(**************************************************************************************************)
subsection‹Hensel's Lemma for ‹p›-adic fields›
(**************************************************************************************************)
(**************************************************************************************************)

theorem hensels_lemma:
  assumes "f ∈ carrier (UP Qp)"
  assumes "a ∈ 𝒪p"
  assumes "gauss_norm f ≥ 0"
  assumes "val (f∙a) > 2*val ((pderiv f)∙a)"
  shows "∃!α ∈ 𝒪p. f∙α = 𝟬 ∧ val (a ⊖ α) > val ((pderiv f)∙a)"
proof-
  have a_closed: "a ∈ carrier Qp"
    using assms val_ring_memE by auto
  have f_nonzero: "f ≠ 𝟬⇘UP Qp⇙"
  proof(rule ccontr)
    assume N: "¬ f ≠ 𝟬⇘UP Qp⇙"
    then have 0: "pderiv f = 𝟬⇘UP Qp⇙"
      using UPQ.deg_zero UPQ.pderiv_deg_0 by blast
    have 1: "f = 𝟬⇘UP Qp⇙"
      using N by auto
    have 2: "eint 2 * val (UPQ.pderiv 𝟬⇘UP Qp⇙ ∙ a) = ∞"
      by (simp add: UPQ.to_fun_zero local.a_closed local.val_zero)
    show False using assms a_closed
      unfolding 2 1
      using eint_ord_simps(6) by blast
  qed
  obtain h where h_def: "h = to_Zp_poly f"
    by blast
  have h_closed: "h ∈ carrier (UP Zp)"
    unfolding h_def using assms
    by (simp add: to_Zp_poly_closed)
  have h_deriv: "Zp.pderiv h = to_Zp_poly (pderiv f)"
    unfolding h_def
    using to_Zp_poly_pderiv[of f] assms by auto
  have 0: "to_Zp (f∙a) = to_function Zp h (to_Zp a)"
    unfolding h_def
    using assms a_closed
    by (simp add: UPQ.to_fun_def to_Zp_poly_eval)
  have 1: "to_Zp ((pderiv f)∙a) = to_function Zp (Zp.pderiv h) (to_Zp a)"
    unfolding h_deriv
    using assms a_closed  UPQ.pderiv_closed UPQ.to_fun_def eint_ord_trans gauss_norm_pderiv to_Zp_poly_eval
    by presburger
  have 2: "val (f∙a) = val_Zp (to_function Zp h (to_Zp a))"
  proof-
    have 20: "f∙a ∈ 𝒪p"
      using assms positive_gauss_norm_eval by blast
    have 21: "val (f∙a) = val_Zp (to_Zp (f∙a))"
      using 20 by (simp add: to_Zp_val)
    show ?thesis unfolding 21 0 by blast
  qed
  have 3: "val ((pderiv f)∙a) = val_Zp ( to_function Zp (Zp.pderiv h) (to_Zp a))"
  proof-
    have 30: "(pderiv f)∙a ∈ 𝒪p"
      using positive_gauss_norm_eval assms gauss_norm_pderiv
      by (meson UPQ.pderiv_closed eint_ord_trans)
    have 31: "val ((pderiv f)∙a) = val_Zp (to_Zp ((pderiv f)∙a))"
      using 30 by (simp add: to_Zp_val)
    show ?thesis unfolding 31 1 by blast
  qed
  have 4: "∃!α. α ∈ carrier Zp ∧
        Zp.to_fun (to_Zp_poly f) α = 𝟬⇘Zp⇙ ∧
        val_Zp (Zp.to_fun (Zp.pderiv (to_Zp_poly f)) (to_Zp a))
        < val_Zp (to_Zp a ⊖⇘Zp⇙ α)"
    apply(rule hensels_lemma')
    using h_closed h_def apply blast
    using assms local.a_closed to_Zp_closed apply blast
    using assms unfolding 2 3 h_def Zp.to_fun_def by blast
  obtain α where α_def: "α ∈ carrier Zp ∧
        Zp.to_fun (to_Zp_poly f) α = 𝟬⇘Zp⇙ ∧
        val_Zp (Zp.to_fun (Zp.pderiv (to_Zp_poly f)) (to_Zp a))
        < val_Zp (to_Zp a ⊖⇘Zp⇙ α)
        ∧ (∀x.  x ∈ carrier Zp ∧
        Zp.to_fun (to_Zp_poly f) x = 𝟬⇘Zp⇙ ∧
        val_Zp (Zp.to_fun (Zp.pderiv (to_Zp_poly f)) (to_Zp a))
        < val_Zp (to_Zp a ⊖⇘Zp⇙ x) ⟶ x = α)"
    using 4 by blast
  obtain β where β_def: "β = ι α"
    by blast
  have β_closed: "β ∈ 𝒪p"
    using α_def unfolding β_def by simp
  have 5: "(Zp.to_fun (to_Zp_poly f) α) = to_Zp (f∙β)"
    using β_closed to_Zp_poly_eval[of f β] assms
    unfolding β_def UPQ.to_fun_def
    by (simp add: Zp.to_fun_def α_def inc_to_Zp)
  have 6: "to_Zp (f∙β) = 𝟬⇘Zp⇙"
    using 5 α_def by auto
  have β_closed: "β ∈ 𝒪p"
    unfolding β_def using α_def  by simp
  have 7: "(f∙β) = 𝟬"
    using 6 assms unfolding β_def
    by (metis β_closed β_def inc_of_zero positive_gauss_norm_eval to_Zp_inc)
  have 8: "α = to_Zp β"
    unfolding β_def using α_def
    by (simp add: inc_to_Zp)
  have 9: "to_Zp a ⊖⇘Zp⇙ α = to_Zp (a ⊖ β)"
    unfolding 8 using assms(2) β_closed
    by (simp add: to_Zp_minus)
  have 10: "val (a ⊖ β) = val_Zp (to_Zp a ⊖⇘Zp⇙ α)"
    unfolding 9 using β_closed assms(2)
    to_Zp_val val_ring_minus_closed by presburger
  have 11: "val (a ⊖ β) > val ((pderiv f)∙a)"
    using α_def unfolding 9 10 3 h_def
    by (simp add: Zp.to_fun_def)
  have 12: "β ∈ 𝒪p ∧ f ∙ β = 𝟬 ∧ val (UPQ.pderiv f ∙ a) < val (a ⊖ β)"
    using "11" "7" β_closed by linarith
  have 13: "∀x. x∈ 𝒪p ∧ f ∙ x = 𝟬 ∧ val (UPQ.pderiv f ∙ a) < val (a ⊖ x)
            ⟶ x = β"
  proof(rule, rule)
    fix x assume A: "x ∈ 𝒪p ∧  f ∙ x = 𝟬 ∧ val (UPQ.pderiv f ∙ a) < val (a ⊖ x)"
    obtain y where y_def: "y = to_Zp x"
      by blast
    have y_closed: "y ∈ carrier Zp"
      unfolding y_def using A
      by (simp add: to_Zp_closed val_ring_memE(2))
    have eval: "Zp.to_fun (to_Zp_poly f) y = 𝟬⇘Zp⇙"
      unfolding y_def using A assms
      by (metis UPQ.to_fun_def Zp.to_fun_def to_Zp_poly_eval to_Zp_zero)
    have 0: "to_Zp a ⊖⇘Zp⇙ y = to_Zp (a ⊖ x)"
      unfolding y_def using A assms
      by (simp add: to_Zp_minus)
    have q: " val_Zp (Zp.to_fun (Zp.pderiv (to_Zp_poly f)) (to_Zp a)) = val (UPQ.pderiv f ∙ a)"
      by (simp add: "3" Zp.to_fun_def h_def)
    have 1: "y ∈ carrier Zp ∧
        Zp.to_fun (to_Zp_poly f) y = 𝟬⇘Zp⇙ ∧
        val_Zp (Zp.to_fun (Zp.pderiv (to_Zp_poly f)) (to_Zp a))
        < val_Zp (to_Zp a ⊖⇘Zp⇙ y)"
      unfolding 0 eval Zp.to_fun_def h_def
      apply(intro conjI y_closed)
      using eval Zp.to_fun_def apply (simp; fail)
      using A unfolding 0 eval Zp.to_fun_def h_def 3
      using assms(2) to_Zp_val val_ring_minus_closed by presburger
    have 2: "y = α"
      using 1 α_def by blast
    show "x = β"
      using y_def unfolding 2 8 using A β_closed
      by (metis to_Zp_inc)
  qed
  show "∃!α. α ∈ 𝒪p ∧ f ∙ α = 𝟬 ∧ val (UPQ.pderiv f ∙ a) < val (a ⊖ α)"
    using 12 13 by metis
qed

lemma nth_root_poly_root_fixed:
  assumes "(n::nat) > 1"
  assumes "a ∈ 𝒪p"
  assumes "val (𝟭 ⊖⇘Qp⇙ a) > 2* val ([n]⋅𝟭)"
  shows "(∃! b ∈ 𝒪p. (b[^]n) = a ∧  val (b ⊖ 𝟭) > val ([n]⋅𝟭))"
proof-
  obtain f where f_def: "f = up_ring.monom (UP Qp) 𝟭 n ⊖⇘UP Qp⇙ up_ring.monom (UP Qp) a 0"
    by blast
  have f_closed: "f ∈ carrier (UP Qp)"
    unfolding f_def apply(rule UPQ.P.ring_simprules)
     apply (simp; fail)   using assms
    by (simp add: val_ring_memE(2))
  have 0: "UPQ.pderiv (up_ring.monom (UP Qp) a 0) = 𝟬⇘UP Qp⇙"
    using assms
    by (simp add: val_ring_memE(2))
  have 1: "UPQ.pderiv (up_ring.monom (UP Qp) (𝟭) n) = (up_ring.monom (UP Qp) ([n]⋅𝟭) (n-1)) "
    using UPQ.pderiv_monom by blast
  have 2: "up_ring.monom (UP Qp) 𝟭 n ∈ carrier (UP Qp)"
    by simp
  have 3: "up_ring.monom (UP Qp) a 0 ∈ carrier (UP Qp)"
    using assms val_ring_memE by simp
  have 4: "UPQ.pderiv f  = up_ring.monom (UP Qp) ([n] ⋅ 𝟭) (n - 1)  ⊖⇘UP Qp⇙ 𝟬⇘UP Qp⇙"
    using 2 3 assms val_ring_memE UPQ.pderiv_minus[of "up_ring.monom (UP Qp) 𝟭 n" "up_ring.monom (UP Qp) a 0"]
    unfolding f_def 0 1 by blast
  have 5: "UPQ.pderiv f = (up_ring.monom (UP Qp) ([n]⋅𝟭) (n-1))"
    unfolding 4 a_minus_def by simp
  have a_closed: "a ∈ carrier Qp"
    using assms val_ring_memE by blast
  have 6: "UPQ.pderiv f ∙ 𝟭 = [n]⋅𝟭 ⊗ 𝟭[^](n-1)"
    unfolding 5 using a_closed
    by (simp add: UPQ.to_fun_monom)
  have 7: "val (𝟭 ⊖⇘Qp⇙ a) > val 𝟭"
  proof-
    have "eint 2 * val ([n] ⋅ 𝟭) ≥ 0"
      by (meson eint_ord_trans eint_pos_int_times_ge val_of_nat_inc zero_less_numeral)
    thus ?thesis
      using assms unfolding val_one
      by (simp add: Qp_def)
  qed
  hence 8: "val a = val 𝟭"
    using a_closed
    by (metis Qp.cring_simprules(6) ultrametric_equal_eq')
  have 9:"val (a [^] (n - 1)) = 0"
    by (simp add: "8" local.a_closed val_zero_imp_val_pow_zero)
  have 10: "val ([n]⋅𝟭 ⊗ 𝟭[^](n-1)) = val ([n]⋅𝟭)"
    unfolding val_one 9 by simp
  have 11: "0 ≤ gauss_norm f"
  proof-
    have p0: "gauss_norm (up_ring.monom (UP Qp) 𝟭 n) ≥ 0"
      using gauss_norm_monom by simp
    have p1: "gauss_norm (up_ring.monom (UP Qp) a 0) ≥ 0"
      using gauss_norm_monom assms val_ring_memE by simp
    have p2: "min (gauss_norm (up_ring.monom (UP Qp) 𝟭 n)) (gauss_norm (up_ring.monom (UP Qp) a 0)) ≥ 0"
      using p0 p1 by simp
    have p3: "0 ≤ gauss_norm
      (up_ring.monom (UP Qp) 𝟭 n ⊖⇘UP Qp⇙ up_ring.monom (UP Qp) a 0)"
      using gauss_norm_ultrametric'[of "up_ring.monom (UP Qp) 𝟭 n" "up_ring.monom (UP Qp) a 0"]
            p2  "2" "3" eint_ord_trans  by blast
    show ?thesis using p3 unfolding f_def by simp
  qed
  have 12: "⋀α. α ∈ 𝒪p ⟹ f ∙ α = α[^]n ⊖ a"
    unfolding f_def using a_closed
    by (simp add: UPQ.to_fun_const UPQ.to_fun_diff UPQ.to_fun_monic_monom val_ring_memE(2))
  have 13: "∃!α. α ∈ 𝒪p ∧ f ∙ α = 𝟬 ∧ val (UPQ.pderiv f ∙ 𝟭) < val (𝟭 ⊖ α)"
    apply(rule hensels_lemma, rule f_closed, rule one_in_val_ring, rule 11)
    unfolding 6 10
    using a_closed assms 12[of 𝟭] assms(3)
    by (simp add: one_in_val_ring)
  have 14: "⋀α. α ∈ 𝒪p ⟹ α[^]n = a ⟷ f ∙ α = 𝟬"
    unfolding f_def using a_closed 12 f_def val_ring_memE(2) by auto
  have 15: "val (UPQ.pderiv f ∙ 𝟭) = val ([n]⋅𝟭)"
    unfolding 6 10 by auto
  have 16: "⋀α. α ∈ 𝒪p ⟹ val (𝟭 ⊖ α) = val (α ⊖ 𝟭)"
  proof-
    have 17: "⋀α. α ∈ 𝒪p ⟹ (𝟭 ⊖ α) = ⊖ (α ⊖ 𝟭)"
      using val_ring_memE
      by (meson Qp.minus_a_inv Qp.one_closed)
    show "⋀α. α ∈ 𝒪p ⟹ val (𝟭 ⊖ α) = val (α ⊖ 𝟭)"
      unfolding 17
      using Qp.minus_closed Qp.one_closed val_minus val_ring_memE(2) by presburger
  qed
  show ?thesis using 13 unfolding 15 using 14 16 Qp.one_closed val_ring_memE(2) by metis
qed

lemma mod_zeroE:
  assumes "(a::int) mod k  = 0"
  shows "∃l. a = l*k"
  using assms
  using Groups.mult_ac(2) by blast

lemma to_Zp_poly_closed':
  assumes "g ∈ carrier (UP Qp)"
  assumes "⋀i. g i ∈ 𝒪p"
  shows "to_Zp_poly g ∈ carrier (UP Zp)"
proof(rule to_Zp_poly_closed)
  show "g ∈ carrier (UP Qp)"
    using assms(1) by blast
  show "0 ≤ gauss_norm g"
  proof-
    have "⋀i. val (g i) ≥ 0"
      using assms val_ring_memE by blast
    thus ?thesis unfolding gauss_norm_def
      by (metis  gauss_norm_coeff_norm gauss_norm_def)
  qed
qed

lemma to_Zp_poly_eval_to_Zp:
  assumes "g ∈ carrier (UP Qp)"
  assumes "⋀i. g i ∈ 𝒪p"
  assumes "a ∈ 𝒪p"
  shows "to_function Zp (to_Zp_poly g) (to_Zp a) = to_Zp (g ∙ a)"
proof-
  have "(∀i. g i ∈ 𝒪p) ⟶ to_function Zp (to_Zp_poly g) (to_Zp a) = to_Zp (g ∙ a)"
    apply(rule UPQ.poly_induct[of g]) using assms apply blast
  proof
    fix p assume A: "p ∈ carrier (UP Qp)" "deg Qp p = 0" "∀i. p i ∈ 𝒪p"
    obtain c where c_def: "c ∈ carrier Qp ∧ p = up_ring.monom (UP Qp) c  0"
      using A  by (metis UPQ.ltrm_deg_0 val_ring_memE(2))
    have 0: "to_Zp_poly (up_ring.monom (UP Qp) c  0) = up_ring.monom (UP Zp) (to_Zp c) 0"
      unfolding to_Zp_poly_def proof fix n show " to_Zp (up_ring.monom (UP Qp) c 0 n) = up_ring.monom (UP Zp) (to_Zp c) 0 n"
        using UP_ring.cfs_monom[of Zp "to_Zp c" 0 n] UP_ring.cfs_monom[of Qp c 0 n] to_Zp_closed[of c ]
        unfolding UP_ring_def
        apply(cases "0 = n")
        using UPQ.cfs_monom Zp.cfs_monom c_def apply presburger
         using UPQ.cfs_monom Zp.cfs_monom c_def
         using to_Zp_zero by presburger
    qed
    have p_eq: "p = up_ring.monom (UP Qp) c  0"
      using c_def by blast
    have 1: "(up_ring.monom (UP Qp) c 0 ∙ a) = c"
      using UPQ.to_fun_to_poly[of c a]  c_def assms val_ring_memE
      unfolding to_polynomial_def  by blast
    show "to_function Zp (to_Zp_poly p) (to_Zp a) = to_Zp (p ∙ a)"
      using c_def assms(3) val_ring_memE(2)[of a]
      UP_cring.to_fun_to_poly[of Zp "to_Zp c" "to_Zp a"]
      unfolding p_eq 0 1 Zp.to_fun_def to_polynomial_def
      using Zp.UP_cring_axioms to_Zp_closed by blast
  next
    show "⋀p. (⋀q. q ∈ carrier (UP Qp) ⟹
              deg Qp q < deg Qp p ⟹ (∀i. q i ∈ 𝒪p) ⟶ to_function Zp (to_Zp_poly q) (to_Zp a) = to_Zp (q ∙ a)) ⟹
         p ∈ carrier (UP Qp) ⟹ 0 < deg Qp p ⟹ (∀i. p i ∈ 𝒪p) ⟶ to_function Zp (to_Zp_poly p) (to_Zp a) = to_Zp (p ∙ a)"
    proof  fix p
      assume A: "(⋀q. q ∈ carrier (UP Qp) ⟹
              deg Qp q < deg Qp p ⟹ (∀i. q i ∈ 𝒪p) ⟶ to_function Zp (to_Zp_poly q) (to_Zp a) = to_Zp (q ∙ a))"
            "p ∈ carrier (UP Qp)" "0 < deg Qp p" "∀i. p i ∈ 𝒪p"
      show "to_function Zp (to_Zp_poly p) (to_Zp a) = to_Zp (p ∙ a)"
      proof-
        obtain q where q_def: "q = truncate Qp  p"
          by blast
        have  q_closed: "q ∈ carrier (UP Qp)"
          unfolding q_def by(rule UPQ.trunc_closed, rule A)
        obtain c where c_def: "c = UPQ.lcf p"
          by blast
        obtain n where n_def: "n = deg Qp p"
          by blast
        have 0: "p = q ⊕⇘UP Qp⇙ up_ring.monom (UP Qp) c n"
          unfolding c_def n_def q_def
          using A(2) UPQ.trunc_simps(1) by blast
        have 1: "up_ring.monom (UP Qp) c n ∈ carrier  (UP Qp)"
          using A(2) UPQ.ltrm_closed c_def n_def by blast
        have 2: "p ∙ a  = q  ∙ a ⊕ (c ⊗ a[^]n)"
          unfolding 0 using assms val_ring_memE
          by (metis "1" A(4) UPQ.to_fun_monom UPQ.to_fun_plus c_def q_closed)
        have 3: "⋀i. i < n ⟹ q i = p i"
          unfolding n_def q_def
          using A(2) UPQ.trunc_cfs by blast
        have 4: "deg Qp q < n"
          unfolding n_def q_def using A
          using UPQ.trunc_degree by presburger
        have 5: "⋀i. i ≥ n ⟹ i >  deg Qp q"
          using A[of ] less_le_trans[of "deg Qp q" "deg Qp p"] unfolding q_def n_def
          using "4" n_def q_def by blast
        have 6: "⋀i. i ≥ n ⟹ q i = 𝟬"
          using q_closed 5 UPQ.deg_leE by blast
        have 7: "(∀i. q i ∈ 𝒪p) ⟶ to_function Zp (to_Zp_poly q) (to_Zp a) = to_Zp (q ∙ a)"
          apply(rule   A) unfolding q_def
          using q_closed q_def apply blast
          using "4" n_def q_def by blast
        have 8: "(∀i. q i ∈ 𝒪p)"
        proof fix i show "q i ∈ 𝒪p" apply(cases "i < n")
            using 3 A(4) apply blast using 6[of i]
            by (metis less_or_eq_imp_le linorder_neqE_nat zero_in_val_ring)
        qed
        have 9: "to_function Zp (to_Zp_poly q) (to_Zp a) = to_Zp (q ∙ a)"
          using 7 8 by blast
        have 10: "to_Zp_poly p = to_Zp_poly q ⊕⇘UP Zp⇙ to_Zp_poly (up_ring.monom (UP Qp) c n)"
        proof fix x
          have 100: "to_Zp_poly (up_ring.monom (UP Qp) c n) = (up_ring.monom (UP Zp) (to_Zp c) n)"
            using to_Zp_poly_monom[of c] A(4) c_def by blast
          have 101: "deg Zp (to_Zp_poly q) ≤ n-1"
              apply(rule  UP_cring.deg_leqI)
              unfolding UP_cring_def using Zp.R_cring apply auto[1]
              using to_Zp_poly_closed' 8 q_closed apply blast
              unfolding to_Zp_poly_def using 4 6
              by (simp add: to_Zp_zero)
          have 102: "(to_Zp_poly q) ∈ carrier (UP Zp)"
            apply(rule to_Zp_poly_closed', rule q_closed) using 8 by blast
          have 103: "deg Zp (to_Zp_poly q) < n"
            using 101 4 by linarith
            have T0: "(to_Zp_poly q ⊕⇘UP Zp⇙ to_Zp_poly (up_ring.monom (UP Qp) c n)) x =
                    (to_Zp_poly q x) ⊕⇘Zp⇙ (to_Zp_poly (up_ring.monom (UP Qp) c n) x)"
              apply(rule  UP_ring.cfs_add)
                apply (simp add: Zp.is_UP_ring)
               apply (simp add: "102")
              using "100" A(2) UPQ.lcf_closed c_def to_Zp_closed by auto
            have c_closed: "c ∈ 𝒪p"
              unfolding c_def  using A(4) by blast
            have to_Zp_c_closed: "to_Zp c ∈ carrier Zp"
              using c_closed to_Zp_closed val_ring_memE(2) by blast
          show "to_Zp_poly p x = (to_Zp_poly q ⊕⇘UP Zp⇙ to_Zp_poly (up_ring.monom (UP Qp) c n)) x"
          proof(cases "x < n")
            case True
            have T1: "(to_Zp_poly (up_ring.monom (UP Qp) c n) x) = 𝟬⇘Zp⇙"
              using True UP_ring.cfs_monom[of Zp] unfolding UP_ring_def
              by (simp add: A(2) UPQ.ltrm_cfs c_def n_def to_Zp_poly_def to_Zp_zero)
            have T2: "to_Zp (p x) = to_Zp (q x)" using 3[of x] True by smt
            have T3: "to_Zp (p x) ∈ carrier Zp"
              apply(rule to_Zp_closed) using A(2) UPQ.UP_car_memE(1) by blast
            show ?thesis using T3
              unfolding T0  unfolding T1 unfolding  to_Zp_poly_def  T2
              using Zp.cring_simprules(8) add_comm by presburger
          next
            case False
            have F: "q x = 𝟬 "
              using False
              by (metis "6" less_or_eq_imp_le linorder_neqE_nat)
            have F': "(to_Zp_poly q) x = 𝟬⇘Zp⇙"
             unfolding to_Zp_poly_def F using to_Zp_zero by blast
            show "to_Zp_poly p x = (to_Zp_poly q ⊕⇘UP Zp⇙ to_Zp_poly (up_ring.monom (UP Qp) c n)) x"
            proof(cases "x = n")
              case True
              have T1: "to_Zp (p x) ∈ carrier Zp"
                apply(rule to_Zp_closed)
                using A(2) UPQ.UP_car_memE(1) by blast
              have T2: "(to_Zp_poly (up_ring.monom (UP Qp) c n) x) = to_Zp c"
                unfolding 100 using UP_ring.cfs_monom[of Zp "to_Zp c" n n] unfolding UP_ring_def True
                using Zp.ring_axioms to_Zp_c_closed by presburger
              show ?thesis using to_Zp_c_closed unfolding T0 F' T2 unfolding to_Zp_poly_def True c_def n_def
                using Zp.cring_simprules(8) by presburger
            next
              case FF: False
              have F0: "p x = 𝟬"
                using FF False unfolding n_def
                using A(2) UPQ.UP_car_memE(2) linorder_neqE_nat by blast
              have F1: "q x = 𝟬"
                using FF False F by linarith
              have F2: "(up_ring.monom (UP Qp) c n) x = 𝟬"
                using FF False A(2) UPQ.cfs_closed UPQ.cfs_monom c_def by presburger
              show ?thesis unfolding T0 unfolding to_Zp_poly_def F0 F1 F2
                using Zp.r_zero Zp.zero_closed to_Zp_zero by presburger
            qed
          qed
        qed
        have 11: "deg Zp (to_Zp_poly q) ≤ n-1"
          apply(rule  UP_cring.deg_leqI)
          unfolding UP_cring_def using Zp.R_cring apply auto[1]
          using to_Zp_poly_closed' 8 q_closed apply blast
          unfolding to_Zp_poly_def using 4 6
          by (smt diff_commute diff_diff_cancel less_one less_or_eq_imp_le linorder_neqE_nat to_Zp_zero zero_less_diff)
        have 12: "(to_Zp_poly q) ∈ carrier (UP Zp)"
          apply(rule to_Zp_poly_closed', rule q_closed) using 8 by blast
        have 13: "deg Zp (to_Zp_poly q) < n"
          using 11 4 by linarith
        have 14: "to_Zp_poly (up_ring.monom (UP Qp) c n) = (up_ring.monom (UP Zp) (to_Zp c) n)"
          using to_Zp_poly_monom[of c] A(4) c_def by blast
        have 15: "Zp.to_fun (to_Zp_poly q ⊕⇘UP Zp⇙ to_Zp_poly (up_ring.monom (UP Qp) c n)) (to_Zp a)=
            Zp.to_fun (to_Zp_poly q) (to_Zp a) ⊕⇘Zp⇙ Zp.to_fun (to_Zp_poly (up_ring.monom (UP Qp) c n)) (to_Zp a)"
          apply(rule Zp.to_fun_plus)
          unfolding 14  apply(rule UP_ring.monom_closed)
          unfolding UP_ring_def
             apply (simp add: Zp.ring_axioms)
            apply (simp add: A(2) UPQ.cfs_closed c_def to_Zp_closed)
           using "12" apply blast
          apply(rule to_Zp_closed) using assms val_ring_memE by blast
        have 16: "to_Zp (q ∙ a ⊕ c ⊗ a [^] n) = to_Zp (q ∙ a)  ⊕⇘Zp⇙ to_Zp (c ⊗ a [^] n)"
          apply(rule to_Zp_add)
           apply(rule val_ring_poly_eval, rule q_closed)
            using "8" apply blast
             apply(rule assms)
            apply(rule val_ring_times_closed)
            unfolding c_def using A(4) apply blast
          by(rule val_ring_nat_pow_closed, rule assms)
        have  17: " to_function Zp (up_ring.monom (UP Zp) (to_Zp c) n) (to_Zp a) =  to_Zp (c ⊗ a [^] n)"
          proof-
            have 170: "to_Zp (c ⊗ a [^] n) = to_Zp c ⊗⇘Zp⇙ to_Zp (a [^] n)"
              apply(rule  to_Zp_mult[of c "a[^]n"])
              unfolding c_def using A(4) apply blast
              by(rule val_ring_nat_pow_closed, rule assms)
            have 171: "to_Zp (a [^] n) = (to_Zp a [^]⇘Zp⇙n)"
              by(rule to_Zp_nat_pow, rule assms)
            have 172: "to_Zp c ∈ carrier Zp "
              apply(rule to_Zp_closed) unfolding c_def
              using A(2) UPQ.UP_car_memE(1) by blast
            have 173: "to_Zp a ∈ carrier Zp "
              apply(rule to_Zp_closed) using assms val_ring_memE by blast
            show ?thesis
              using 172 173 Zp.to_fun_monom[of "to_Zp c" "to_Zp a" n] unfolding Zp.to_fun_def 170 171
              by blast
        qed
        show ?thesis
          using 15 unfolding Zp.to_fun_def 10 2 16 9 unfolding 14 17
          by blast
      qed
    qed
  qed
  thus ?thesis using assms by blast
qed

lemma inc_nat_pow:
  assumes "a ∈ carrier Zp"
  shows "ι ([(n::nat)] ⋅⇘Zp⇙a) = [n]⋅(ι a)"
  apply(induction n)
  apply (metis Qp_def Qp.int_inc_zero Qp.nat_mult_zero Zp.add.nat_pow_0 Zp_int_inc_zero' ι_def frac_inc_of_int)
  unfolding Qp.add.nat_pow_Suc Zp.add.nat_pow_Suc
  using Zp_nat_mult_closed assms inc_of_sum by presburger

lemma poly_inc_pderiv:
  assumes "g ∈ carrier (UP Zp)"
  shows "poly_inc (Zp.pderiv g) = UPQ.pderiv (poly_inc g)"
proof fix x
  have 0: "UPQ.pderiv (poly_inc g) x = [Suc x] ⋅ poly_inc g (Suc x)"
    apply(rule UPQ.pderiv_cfs[of "poly_inc g" x])
    by(rule poly_inc_closed, rule assms)
  have 1: "Zp.pderiv g x = [Suc x] ⋅⇘Zp⇙ g (Suc x)"
    by(rule Zp.pderiv_cfs[of g x], rule assms)
  show "poly_inc (Zp.pderiv g) x = UPQ.pderiv (poly_inc g) x"
    unfolding 0  unfolding poly_inc_def 1 apply(rule  inc_nat_pow)
    using Zp.UP_car_memE(1) assms by blast
qed

lemma Zp_hensels_lemma:
  assumes "f ∈ carrier Zp_x"
  assumes "a ∈ carrier Zp"
  assumes "Zp.to_fun (Zp.pderiv f) a ≠ 𝟬⇘Zp⇙"
  assumes "Zp.to_fun f a ≠ 𝟬⇘Zp ⇙"
  assumes "val_Zp (Zp.to_fun f a) > eint 2 * val_Zp (Zp.to_fun (Zp.pderiv f) a)"
  obtains α where
       "Zp.to_fun f α = 𝟬⇘Zp⇙" and "α ∈ carrier Zp"
       "val_Zp (a ⊖⇘Zp⇙ α) > val_Zp (Zp.to_fun (Zp.pderiv f) a)"
       "val_Zp (a ⊖⇘Zp⇙ α) = val_Zp (divide (Zp.to_fun f a) (Zp.to_fun (Zp.pderiv f) a))"
       "val_Zp (Zp.to_fun (Zp.pderiv f) α) = val_Zp (Zp.to_fun (Zp.pderiv f) a)"
proof-
  have "hensel p f a"
    using assms
    by (simp add: Zp_def hensel.intro hensel_axioms.intro padic_integers_axioms)
  then show ?thesis
    using hensel.full_hensels_lemma[of p f a] that
    unfolding Zp_def
    by blast
qed

end
end