diff --git a/thys/Crypto_Standards/EC_Common.thy b/thys/Crypto_Standards/EC_Common.thy
--- a/thys/Crypto_Standards/EC_Common.thy
+++ b/thys/Crypto_Standards/EC_Common.thy
@@ -1,1118 +1,1118 @@
 theory EC_Common
   imports
     "Elliptic_Curves_Group_Law.Elliptic_Test"
     "More_Residues"
 begin
 
 section \<open>Edits to Elliptic_Test\<close>
 text \<open>There are a few edits we need to make to the AFP entry we build on here.  First there
 are several variables defined in its last section that we need to ignore.  In particular, we want
 to ignore the definitions of "m", "a", etc. so that we can use those names otherwise.  To be
 entirely safe, and because we don't use these definitions anywhere, we scrub them entirely.\<close>
 
 hide_const Elliptic_Test.m
 hide_fact  Elliptic_Test.m_def
 hide_const Elliptic_Test.a
 hide_fact  Elliptic_Test.a_def
 hide_const Elliptic_Test.b
 hide_fact  Elliptic_Test.b_def
 hide_const Elliptic_Test.gx
 hide_fact  Elliptic_Test.gx_def
 hide_const Elliptic_Test.gy
 hide_fact  Elliptic_Test.gy_def
 hide_const Elliptic_Test.priv
 hide_fact  Elliptic_Test.priv_def
 hide_const Elliptic_Test.pubx
 hide_fact  Elliptic_Test.pubx_def
 hide_const Elliptic_Test.puby
 hide_fact  Elliptic_Test.puby_def
 hide_const Elliptic_Test.order
 hide_fact  Elliptic_Test.order_def
 
 text \<open>The second thing we need to "edit" is this.  We need to be able to use this lemma for
 checking test vectors.  So we need it to be designated with [code].\<close>
 lemmas (in residues_prime_gt2) [code] = on_curve_residues_eq
 
 
 section \<open>EC_Common\<close>
 text \<open>This section has facts about the arithmetic of points on an elliptic curve.\<close>
 
 lemma (in euclidean_semiring_cancel) mod_pow_cong:
   "a mod c = b mod c \<Longrightarrow> (a ^ n) mod c = (b ^ n) mod c"
   by (induction n) (auto intro!: mod_mult_cong)
 
 declare (in domain)    integral_iff[simp]
 declare (in field)      divide_self[simp]
 declare (in field)  divide_eq_0_iff[simp]
 
 lemma (in cring) power2_sum:
   assumes [simp]: "x \<in> carrier R"  "y \<in> carrier R"
   shows   "(x \<oplus> y)[^](2::nat) = x[^](2::nat) \<oplus> y[^](2::nat) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> x \<otimes> y"
 proof -
   have 1: "(2::int) = 1 + 1" by arith
   have 2: "\<guillemotleft>2\<guillemotright> = \<one> \<oplus> \<one>" unfolding 1 of_int_add by simp
   show ?thesis
     by (simp add: power2_eq_square 2 minus_eq l_distr r_distr a_ac m_ac minus_add r_minus)
 qed
 
 lemma (in ring) diff_same[simp]: "a \<in> carrier R \<Longrightarrow> a \<ominus> a = \<zero>"
   using eq_diff0 by force
 
 lemma (in cring) power2_diff:
   assumes [simp]: "x \<in> carrier R"  "y \<in> carrier R"
   shows   "(x \<ominus> y)[^](2::nat) = x[^](2::nat) \<oplus> y[^](2::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> x \<otimes> y"
 proof -
   have 1: "(2::int) = 1 + 1" by arith
   have 2: "\<guillemotleft>2\<guillemotright> = \<one> \<oplus> \<one>"
     unfolding 1 of_int_add by simp
   show ?thesis
     by (simp add: power2_eq_square 2 minus_eq l_distr r_distr a_ac m_ac minus_add r_minus)
 qed
 
 lemma (in ring) power3_eq_cube:
   "x \<in> carrier R \<Longrightarrow> x[^]\<^bsub>R\<^esub>(3::nat) = x \<otimes>\<^bsub>R\<^esub> x \<otimes>\<^bsub>R\<^esub> x"
   by (simp add: numeral_3_eq_3)
 
 lemma (in ring) zero_pow_nat[simp]: "n \<noteq> 0 \<Longrightarrow> \<zero>\<^bsub>R\<^esub> [^]\<^bsub>R\<^esub> (n::nat) = \<zero>\<^bsub>R\<^esub>"
   using nat_pow_zero by blast
 
 lemma (in comm_group) m_one_iff: "p \<in> carrier G \<Longrightarrow> q \<in> carrier G \<Longrightarrow> p \<otimes> q = \<one> \<longleftrightarrow> p = inv q"
   using local.inv_equality by auto
 
 lemma (in residues) res_diff_eq: "x \<ominus> y = (x - y) mod m"
   unfolding a_minus_def diff_conv_add_uminus res_neg_eq res_add_eq by (simp add: mod_simps)
 
 lemma (in field) nonzero_mult_divide_mult_cancel_left' [simp]:
   assumes [simp]: "a \<in> carrier R"  "b \<in> carrier R"  "c \<in> carrier R"  "b \<noteq> \<zero>"  "c \<noteq> \<zero>"
   shows   "(a \<otimes> c) \<oslash> (b \<otimes> c) = a \<oslash> b"
   by (subst (1 2) m_comm) simp_all
 
 lemma (in field) nonzero_mult_divide_divide_cancel_left [simp]:
   assumes [simp]: "a \<in> carrier R"  "b \<in> carrier R"  "c \<in> carrier R"  "b \<noteq> \<zero>"  "c \<noteq> \<zero>"
   shows   "(a \<oslash> c) \<oslash> (b \<oslash> c) = a \<oslash> b"
   by (subst (1 3) m_div_def) (simp add: nonzero_imp_inverse_nonzero)
 
 lemma (in field) l_diff_distr:
   "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> z \<in> carrier R \<Longrightarrow> (x \<ominus> y) \<otimes> z = x \<otimes> z \<ominus> y \<otimes> z"
   using r_diff_distr[of x y z] by (simp add: m_ac)
 
 lemma (in field) l_diff_div_distr:
   "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> z \<in> carrier R \<Longrightarrow> (x \<ominus> y) \<oslash> z = (x \<oslash> z) \<ominus> (y \<oslash> z)"
   by (auto simp: m_div_def l_diff_distr)
 
 lemma (in field) of_natural_nat_pow: "\<guillemotleft>n\<guillemotright>\<^sub>\<nat> [^] (p::nat) = \<guillemotleft>n^p\<guillemotright>\<^sub>\<nat>"
   by (induction p) (auto simp: m_ac)
 
 lemma (in field) of_integer_int[simp]: "\<guillemotleft>int n\<guillemotright> = \<guillemotleft>n\<guillemotright>\<^sub>\<nat>"
   by (induction n) auto
 
 lemma (in field) of_integer_numeral: "\<guillemotleft>numeral n\<guillemotright> = \<guillemotleft>numeral n\<guillemotright>\<^sub>\<nat>"
   apply (subst semiring_1_class.of_nat_numeral[symmetric])
   apply (subst of_integer_int)
   ..
 
 lemma (in field) divide_mult_comm:
   "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow> (a \<oslash> b) \<otimes> c = a \<otimes> (c \<oslash> b)"
   by (subst times_divide_eq_left) (auto simp flip: times_divide_eq_right)
 
 lemma (in field) div_cancel:
   assumes [simp]: "a \<in> carrier R"  "b \<in> carrier R"  "c \<in> carrier R"  "c \<noteq> \<zero>"
   shows   "a \<oslash> c = b \<oslash> c \<longleftrightarrow> a = b"
 proof
   assume "a \<oslash> c = b \<oslash> c"
   then have "(a \<oslash> c) \<oslash> inv c  = (b \<oslash> c) \<oslash> inv c"
     by simp
   then show "a = b"
     by (subst (asm) (1 2) nonzero_divide_divide_eq_left)
        (auto simp: nonzero_imp_inverse_nonzero)
 qed simp
 
 lemma (in group) pow_dbl_eq_pow_of_prime_ord_gt_2:
   "e \<in> carrier G \<Longrightarrow> prime (ord e) \<Longrightarrow> ord e > 2 \<Longrightarrow> e [^] (2 * n :: nat) = \<one> \<longleftrightarrow> e [^] n = \<one>"
   by (subst (1 2) pow_eq_id)
      (auto simp: prime_dvd_mult_nat)
 
 lemma (in ring) add_eq_iff_eq_minus:
   "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> a \<oplus> b = c \<longleftrightarrow> a = c \<ominus> b"
   by (metis a_minus_def add.inv_solve_right)
 
 lemma (in field) mult_eq_iff_eq_divide:
   "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow> a \<otimes> b = c \<longleftrightarrow> a = c \<oslash> b"
   by (metis (full_types) cring_simprules(14) div_closed divide_mult_comm l_one 
         local.divide_self m_lcancel)
 
 lemma (in field) eq_mult_iff_divide_eq:
   "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow> c = a \<otimes> b \<longleftrightarrow> c \<oslash> b = a"
   by (metis mult_eq_iff_eq_divide)
 
 lemma (in cring) r_distr_diff:
   assumes "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
   shows   "x \<otimes> (y \<ominus> z) = x \<otimes> y \<ominus> x \<otimes> z"
   using assms by (simp add: cring.cring_simprules(15) is_cring r_distr r_minus)
 
 lemma (in field) divide_eq_divide_iff_mult_eq_mult:
   assumes [simp]: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R" "w \<in> carrier R" "y \<noteq> \<zero>" "w \<noteq> \<zero>"
   shows   "x \<oslash> y = z \<oslash> w \<longleftrightarrow> x \<otimes> w = z \<otimes> y"
   by (simp add: mult_eq_iff_eq_divide flip: eq_mult_iff_divide_eq)
 
 lemma (in field) inv_pow_distr:
   assumes "x \<in> carrier R"  "x \<noteq> \<zero>"
   shows   "inv (x[^](k::nat)) = (inv x)[^]k"
   by (metis assms comm_inv_char inv_closed nat_pow_closed nat_pow_one r_inv nat_pow_distrib)
 
 lemma (in field) inv_Suc_pow_cancel:
   assumes "x \<in> carrier R"  "x \<noteq> \<zero>"
   shows   "x \<otimes> (inv x)[^](Suc (k::nat)) = (inv x)[^]k"
   using assms r_inv nat_pow_Suc m_lcomm by fastforce
 
 lemma (in ell_field) xz_coord_padd_simp:
   assumes "on_curvep a b (x1, y1, z)"
     and   "on_curvep a b (x2, y2, z)"
     and   "(x3, y3, z3) = padd a (x1, y1, z) (x2, y2, z)"
     and   ab_in_carrier[simp]: "a \<in> carrier R" "b \<in> carrier R"
     and   "(x2 \<ominus> x1) \<otimes> z \<noteq> \<zero>"
   shows   "x3 = (x2 \<ominus> x1) \<otimes> z[^](4::nat) \<otimes> ((x1 \<otimes> x2 \<oplus> a \<otimes> z[^](2::nat)) 
               \<otimes> (x1 \<oplus> x2) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<otimes> z[^](3::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> y1 \<otimes> y2 \<otimes> z)
          \<and> z3 = (x2 \<ominus> x1)[^](3::nat) \<otimes> z[^](5::nat)"
 proof -
   define u where "u = x2 \<otimes> z \<ominus> x1 \<otimes> z"
   have carrier: "x1 \<in> carrier R" "y1 \<in> carrier R" "x2 \<in> carrier R" "y2 \<in> carrier R" "z \<in> carrier R"
     using assms(1) assms(2) unfolding on_curvep_def by blast+
   then have z_nz: "z \<noteq> \<zero>" using assms(1) assms(6) domain.integral_iff
     unfolding on_curvep_def by force
   have u_nz: "u \<noteq> \<zero>" using assms(1) assms(6) carrier u_def unfolding on_curvep_def
     by (simp add: cring_axioms cring.cring_simprules(14) cring.r_distr_diff)
   have [simp]: "in_carrierp (x1, y1, z)" "in_carrierp (x2, y2, z)"
      using assms(1) assms(2) on_curvep_imp_in_carrierp by blast+
   then have on_curvep3: "on_curvep a b (x3, y3, z3)"
      by (simp add: assms(3) padd_closed assms(1) assms(2))
   then have carrier3: "x3 \<in> carrier R" "y3 \<in> carrier R" "z3 \<in> carrier R"
     using on_curvep_imp_in_carrierp in_carrierp_def by auto
   have p1_ec_eqn: "y1[^](2::nat) \<otimes> z = x1[^](3::nat) \<oplus> a \<otimes> x1 \<otimes> z[^](2::nat) \<oplus> b \<otimes> z[^](3::nat)"
     using assms(1) z_nz prod_cases3 carrier unfolding on_curvep_def by (auto split: prod.splits)
   have p2_ec_eqn: "y2[^](2::nat) \<otimes> z = x2[^](3::nat) \<oplus> a \<otimes> x2 \<otimes> z[^](2::nat) \<oplus> b \<otimes> z[^](3::nat)"
     using assms(2) z_nz prod_cases3 unfolding on_curvep_def by (auto split: prod.splits)
   have z3: "z3 = (x2 \<ominus> x1)[^](3::nat) \<otimes> z[^](5::nat)"
     using assms(3) u_nz z_nz carrier padd_def p1_ec_eqn p2_ec_eqn unfolding u_def Let_def
     by (auto split: prod.splits, field, simp)
   have x3: "x3 = (x2 \<ominus> x1) \<otimes> z[^](4::nat) \<otimes> ((y2[^](2::nat) \<otimes> z)
         \<oplus> (y1[^](2::nat) \<otimes> z) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> y1 \<otimes> y2 \<otimes> z \<ominus> (x1 \<oplus> x2) \<otimes> (x2 \<ominus> x1)[^](2::nat))"
     using assms(3) u_nz z_nz carrier padd_def unfolding u_def Let_def
     by (auto split: prod.splits, field, simp)
   then have x3': "\<dots> = (x2 \<ominus> x1) \<otimes> z[^](4::nat)
     \<otimes> ((x1 \<otimes> x2 \<oplus> a \<otimes> z[^](2::nat)) \<otimes> (x1 \<oplus> x2) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<otimes> z[^](3::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> y1 \<otimes> y2 \<otimes> z)"
     apply (subst p1_ec_eqn, subst p2_ec_eqn) using carrier ab_in_carrier by (field, simp)
   then show ?thesis using x3 x3' z3 by simp
 qed
 
 lemma (in ell_field) pdouble_remove_y_eqn:
   assumes on_curvep: "on_curvep \<guillemotleft>-3\<guillemotright> b (x, y, z)"
     and   [simp]: "b \<in> carrier R"  "z \<noteq> \<zero>"  "y \<noteq> \<zero>"
     and   double: "Point qx qy = make_affine (pdouble \<guillemotleft>-3\<guillemotright> (x, y, z))"
   shows   "qx \<otimes> (\<guillemotleft>2\<guillemotright> \<otimes> y \<otimes> z) [^](2::nat) = 
            (x [^](2::nat) \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> z [^](2::nat)) [^](2::nat) \<ominus> \<guillemotleft>8\<guillemotright> \<otimes> b \<otimes> x \<otimes> z [^](3::nat)"
 proof -
   have in_carrierp[simp]: "x \<in> carrier R"  "y \<in> carrier R"  "z \<in> carrier R"
     using assms(1) on_curvep unfolding on_curvep_def by fast+
   then have "on_curve \<guillemotleft>-3\<guillemotright> b (Point qx qy)"
     using on_curvep double pdouble_closed assms(1) assms(2) assms(3) on_curvep_iff_on_curve
       of_int_closed pdouble_in_carrierp in_carrierp on_curvep_imp_in_carrierp by metis
   define l where "l = \<guillemotleft>2\<guillemotright> \<otimes> y \<otimes> z"
   define m where "m = \<guillemotleft>3\<guillemotright> \<otimes> x [^] (2::nat) \<oplus> \<guillemotleft>-3\<guillemotright> \<otimes> z[^](2::nat)"
   define t where "t = inv (l[^](3::nat))"
   have 0: "l \<noteq> \<zero>" by (simp add: l_def)
   have 1: "l[^](3::nat) \<noteq> \<zero>" by (simp add: l_def)
   then have 2: "t \<otimes> l \<otimes> l[^](2::nat) = \<one>" using t_def l_def
     by (simp add: m_assoc numeral_2_eq_2 numeral_3_eq_3)
   have [simp]: "l \<in> carrier R" "t \<in> carrier R" "m \<in> carrier R"
     using l_def inv_closed l_def m_def t_def m_closed a_closed nat_pow_closed 1 by auto
   then have 3: "qx = (m[^](2::nat) \<ominus> \<guillemotleft>4\<guillemotright> \<otimes> x \<otimes> y \<otimes> l) \<otimes> t \<otimes> l"
     using assms(3) assms(4) double in_carrierp m_comm int_pow_int 0 1 m_div_def t_def
     unfolding make_affine_def pdouble_def Let_def l_def m_def by (simp add: 0 1 m_div_def m_ac)
   then have 4: "qx \<otimes> l[^](2::nat) = m[^](2::nat) \<ominus> \<guillemotleft>4\<guillemotright> \<otimes> x \<otimes> y \<otimes> l" using 2
     by (simp add: 2 m_assoc numeral_2_eq_2 numeral_3_eq_3)
   have 4: "y[^](2::nat) \<otimes> z = x[^](3::nat) \<oplus> \<guillemotleft>-3\<guillemotright> \<otimes> x \<otimes> z[^](2::nat) \<oplus> b \<otimes> z[^](3::nat)"
     using assms unfolding on_curvep_def by fast
   then have 5: "m[^](2::nat) \<ominus> \<guillemotleft>4\<guillemotright> \<otimes> x \<otimes> y \<otimes> l =
                (x[^](2::nat) \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> z[^](2::nat))[^](2::nat) \<ominus> \<guillemotleft>8\<guillemotright> \<otimes> b \<otimes> x \<otimes> z[^](3::nat)"
     unfolding m_def l_def apply (field 4) by (rule TrueI)
   then show ?thesis using 4 l_def 2 3 m_assoc by auto
 qed
 
 lemma (in cring) on_curvep_nz:
   "\<lbrakk>on_curvep a b (x, y, z); z \<noteq> \<zero>\<rbrakk> \<Longrightarrow>
       y [^] (2::nat) \<otimes> z = x [^] (3::nat) \<oplus> a \<otimes> x \<otimes> z [^] (2::nat) \<oplus> b \<otimes> z [^] (3::nat)"
   by (simp add: on_curvep_def)
 
 lemma (in field) on_curvep_nz_identity:
   assumes "on_curvep a b (x, y, z)"  "z \<noteq> \<zero>"  "a \<in> carrier R"  "b \<in> carrier R"
   shows   "(\<guillemotleft>4\<guillemotright> \<otimes> x \<otimes> (x[^](2::nat) \<oplus> a \<otimes> z[^](2::nat)) \<oplus> \<guillemotleft>4\<guillemotright> \<otimes> b \<otimes> z[^](3::nat)) \<otimes> z =
            (\<guillemotleft>2\<guillemotright> \<otimes> y \<otimes> z)[^](2::nat)"
 proof -
   have x: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R" 
     using assms(1) on_curvep_def by simp_all
   have 0: "x [^] (3::nat) \<oplus> a \<otimes> x \<otimes> z [^] (2::nat) \<oplus> b \<otimes> z [^] (3::nat) = y [^] (2::nat) \<otimes> z"
     using assms on_curvep_nz by simp
   have 1: "(\<guillemotleft>4\<guillemotright> \<otimes> x \<otimes> (x[^](2::nat) \<oplus> a \<otimes> z[^](2::nat)) \<oplus> \<guillemotleft>4\<guillemotright> \<otimes> b \<otimes> z[^](3::nat)) \<otimes> z =
            \<guillemotleft>4\<guillemotright> \<otimes> (x[^](3::nat) \<oplus> a \<otimes> x \<otimes> z[^](2::nat) \<oplus> b \<otimes> z[^](3::nat)) \<otimes> z"
     by (field, simp)
   have 2: "\<dots> = \<guillemotleft>4\<guillemotright> \<otimes> y [^] (2::nat) \<otimes> z \<otimes> z" by (simp add: 0 x m_assoc)
   show ?thesis using assms x by (simp add: 1 2, field, simp)
 qed
 
 lemma (in residues_prime) res_inv_mult:
   assumes "z \<noteq> 0"  "z \<in> carrier R"
     shows "z ^ (p - 2) * z mod p = (inv z) * z mod p"
 proof -
   have "\<not> p dvd (nat z)"
     using assms R_def residues.res_carrier_eq residues_axioms nat_dvd_not_less by auto
   then have "z ^ (p - 1) mod p = 1"
     by (metis cong_def dvd_eq_mod_eq_0 int_nat_eq euler_theorem mod_0 nat_int
               of_nat_dvd_iff one_cong p_coprime_right_int res_one_eq prime_totient_eq)
   then show ?thesis
     by (metis R_def Suc_1 Suc_diff_Suc assms l_inv p_prime prime_gt_1_nat res_one_eq
               residues.res_mult_eq residues_axioms semiring_normalization_rules(28) zero_cong)
 qed
 
 lemma (in residues_prime) res_inv_one:
   assumes "z \<noteq> 0"  "z \<in> carrier R"
     shows "z ^ (p - 2) * z mod p = 1"
   using assms res_inv_mult l_inv res_mult_eq res_one_eq res_zero_eq
   by auto
 
 lemma (in residues_prime) res_mult_div:
   assumes "z \<noteq> 0"  "z \<in> carrier R"
     shows "x * z ^ (p - 2) mod p = x \<oslash> z"
 proof -
   have "z \<otimes> inv z = \<one>"
     using assms r_inv zero_cong by blast
   then have "z ^ (p - 2) mod p = (inv z) mod p"
     by (metis assms comm_inv_char mod_in_carrier mult_cong res_mult_eq
               semiring_normalization_rules(7) res_inv_mult)
   then show ?thesis using assms
     by (metis m_div_def mod_mult_right_eq res_mult_eq zero_cong)
 qed
 
 lemma (in residues_prime_gt2) add_pnts_eqn_x:
   assumes p1_on_curve: "on_curve a b (Point x1 y1)"
     and   p2_on_curve: "on_curve a b (Point x2 y2)"
     and   p1_plus_p2: "Point x3 y3 = add a (Point x1 y1) (Point x2 y2)"
     and   nz_cond: "x1 = x2 \<Longrightarrow> y1 = y2"
     and   ab_in_carrier: "a \<in> carrier R"  "b \<in> carrier R"
   shows   "x3 \<otimes> (x2 \<ominus> x1)[^](2::nat) = (a \<oplus> x1 \<otimes> x2) \<otimes> (x1 \<oplus> x2) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> y1 \<otimes> y2"
 proof cases
   assume "x1 = x2"
   with nz_cond p1_on_curve
   have [simp]: "y1 = y2" "x1 = x2" "x2 \<in> carrier R" "y2 \<in> carrier R"
     and *: "y2 [^] (2::nat) = x2 [^] (3::nat) \<oplus> a \<otimes> x2 \<oplus> b"
     by (auto simp add: on_curve_def)
   have "on_curve a b (Point x3 y3)"
     unfolding p1_plus_p2 by (intro add_closed assms)
   then have [simp]: "x3 \<in> carrier R" "y3 \<in> carrier R"
     by (auto simp add: on_curve_def)
 
   show ?thesis
     using *
     apply (simp add: local.power2_eq_square local.m_assoc)
     apply field
     apply simp
     done
 next
   assume nz_cond: "x1 \<noteq> x2"
   have carrier[simp]: "x1 \<in> carrier R" "y1 \<in> carrier R" "x2 \<in> carrier R" "y2 \<in> carrier R"
     using assms(1) assms(2) unfolding on_curve_def by simp_all
   have y1sq: "y1[^](2::nat) = x1[^](3::nat) \<oplus> a \<otimes> x1 \<oplus> b" 
     using p1_on_curve unfolding on_curve_def by simp
   have y2sq: "y2[^](2::nat) = x2[^](3::nat) \<oplus> a \<otimes> x2 \<oplus> b" 
     using p2_on_curve unfolding on_curve_def by simp
   have denom_nz: "(x2 \<ominus> x1)[^](2::nat) \<noteq> \<zero> \<and> (x2 \<ominus> x1)[^](2::nat) \<in> carrier R"
     using nz_cond by auto
   then have r_cancel: "\<forall> z \<in> carrier R. z \<otimes> (x2 \<ominus> x1)[^](2::nat) \<oslash> (x2 \<ominus> x1)[^](2::nat) = z"
     using denom_nz divide_self m_assoc by (metis local.times_divide_eq_right r_one)
   have 0: "x3 = ((y2 \<ominus> y1) \<oslash> (x2 \<ominus> x1))[^](2::nat) \<ominus> (x1 \<oplus> x2)"
     using p1_plus_p2 nz_cond add.m_assoc nz_cond cring_simprules(15) eq_diff0 local.minus_add
     unfolding add_def Let_def by force
   then have 1: "\<dots> = (y2 \<ominus> y1)[^](2::nat) \<oslash> (x2 \<ominus> x1) [^](2::nat) \<ominus> (x1 \<oplus> x2)"
     using nonzero_power_divide nz_cond by auto
   then have "\<dots> = ((y2 \<ominus> y1)[^](2::nat) \<ominus> (x1 \<oplus> x2) \<otimes> (x2 \<ominus> x1)[^](2::nat))
                                                                 \<oslash> (x2 \<ominus> x1)[^](2::nat)"
     using l_diff_distr denom_nz carrier r_cancel by (simp add: m_div_def)
   then have 2:
     "x3 \<otimes> (x2 \<ominus> x1)[^](2::nat) = (y2 \<ominus> y1)[^](2::nat) \<ominus> (x1 \<oplus> x2) \<otimes> (x2 \<ominus> x1)[^](2::nat)"
     using r_cancel 0 1 by (simp add: denom_nz)
   then have "\<dots> = (a \<oplus> x1 \<otimes> x2) \<otimes> (x1 \<oplus> x2) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> y1 \<otimes> y2"
     using p1_on_curve p2_on_curve ab_in_carrier unfolding on_curve_def by (field y1sq y2sq, simp)
   then show ?thesis using 2 by simp
 qed
 
 lemma (in residues_prime_gt2) add_eliminate_ys_simp:
   assumes p1_on_curve: "on_curve a b (Point x1 y1)"
     and   p2_on_curve: "on_curve a b (Point x2 y2)"
     and   p1_plus_p2: "Point x3 y3 = add a (Point x1 y1) (Point x2 y2)"
     and   mp1_plus_p2: "Point xd yd = add a (opp (Point x1 y1)) (Point x2 y2)"
     and   x1_neq_x2: "x1 \<noteq> x2"
     and   ab_in_carrier: "a \<in> carrier R"  "b \<in> carrier R"
   shows   "(x3 \<oplus> xd) \<otimes> (x2 \<ominus> x1)[^](2::nat) = \<guillemotleft>2\<guillemotright> \<otimes> (a \<oplus> x1 \<otimes> x2) \<otimes> (x1 \<oplus> x2) \<oplus> \<guillemotleft>4\<guillemotright> \<otimes> b"
 proof -
   have carrier[simp]: "x1 \<in> carrier R" "y1 \<in> carrier R" "x2 \<in> carrier R" "y2 \<in> carrier R"
     using assms(1) assms(2) unfolding on_curve_def by simp_all
   have "on_curve a b (Point x3 y3)" "on_curve a b (Point xd yd)"
     using p1_plus_p2 mp1_plus_p2 p1_on_curve p2_on_curve opp_closed add_closed
     by (simp add: ab_in_carrier)+
   then have x3_xd_carrier[simp]: "x3 \<in> carrier R" "xd \<in> carrier R"
     unfolding on_curve_def by simp_all
   have x3: "x3 \<otimes> (x2 \<ominus> x1)[^](2::nat) = (a \<oplus> x1 \<otimes> x2) \<otimes> (x1 \<oplus> x2) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> y1 \<otimes> y2"
     using assms add_pnts_eqn_x by blast
   have 0: "on_curve a b (Point x1 (\<ominus> y1))" using p1_on_curve opp_closed opp_def by fastforce
   have "Point xd yd = add a (Point x1 (\<ominus> y1)) (Point x2 y2)"
     using mp1_plus_p2 unfolding opp_def by simp
   then have
     "xd \<otimes> (x2 \<ominus> x1)[^](2::nat) = (a \<oplus> x1 \<otimes> x2) \<otimes> (x1 \<oplus> x2) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> (\<ominus> y1) \<otimes> y2"
     using carrier p1_on_curve p2_on_curve x1_neq_x2 add_pnts_eqn_x minus_minus 0
       cring_simprules(15) ab_in_carrier
     by blast
   then have xd: "xd \<otimes> (x2 \<ominus> x1)[^](2::nat) = (a \<oplus> x1 \<otimes> x2) \<otimes> (x1 \<oplus> x2) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b
                                                 \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> y1 \<otimes> y2"
     by (simp add: cring_simprules(28) cring_simprules(29) local.minus_eq)
   have sum: "(x3 \<oplus> xd) \<otimes> (x2 \<ominus> x1)[^](2::nat) = x3 \<otimes> (x2 \<ominus> x1)[^](2::nat)
                                                    \<oplus> xd \<otimes> (x2 \<ominus> x1)[^](2::nat)"
     using x3_xd_carrier carrier by (field, simp)
   have "\<dots> = \<guillemotleft>2\<guillemotright> \<otimes> (a \<oplus> x1 \<otimes> x2) \<otimes> (x1 \<oplus> x2) \<oplus> \<guillemotleft>4\<guillemotright> \<otimes> b" unfolding x3 xd by (field, simp)
   then show ?thesis using sum by presburger
 qed
 
 named_theorems remove_mod
 
 lemma mmult_mod_mod[remove_mod]: "(a mod m) **\<^bsub>m\<^esub> (b mod m) = (a * b) mod m"
   unfolding mmult_def mod_mult_eq ..
 
 lemma madd_mod_mod[remove_mod]: "(a mod m) ++\<^bsub>m\<^esub> (b mod m) = (a + b) mod m"
   unfolding madd_def mod_add_eq ..
 
 lemma msub_mod_mod[remove_mod]: "(a mod m) --\<^bsub>m\<^esub> (b mod m) = (a - b) mod m"
   unfolding msub_def mod_diff_eq ..
 
 lemma mpow_mod[remove_mod]: "(a mod m) ^^^\<^bsub>m\<^esub> n = (a ^ n) mod m"
   unfolding mpow_def power_mod ..
 
 lemma madd_mod: "(x ++\<^bsub>m\<^esub> y) mod m = x ++\<^bsub>m\<^esub> y"
   by (simp add: madd_def)
 
 lemma msub_same_eq_zero[simp]: "x --\<^bsub>m\<^esub> y = 0 \<longleftrightarrow> x mod m = y mod m"
   by (metis (no_types, opaque_lifting) cancel_ab_semigroup_add_class.diff_right_commute
         eq_iff_diff_eq_0 mod_0 msub_def msub_mod_mod)
 
 definition mpdouble_nz :: "int \<Rightarrow> int \<Rightarrow> int ppoint \<Rightarrow> int ppoint" where
   "mpdouble_nz m a = (\<lambda>(x, y, z).
     let
       l = 2 mod m **\<^bsub>m\<^esub> y **\<^bsub>m\<^esub> z;
       n = 3 mod m **\<^bsub>m\<^esub> x ^^^\<^bsub>m\<^esub> 2 ++\<^bsub>m\<^esub> a **\<^bsub>m\<^esub> z ^^^\<^bsub>m\<^esub> 2
     in
       (l **\<^bsub>m\<^esub> (n ^^^\<^bsub>m\<^esub> 2 --\<^bsub>m\<^esub> 4 mod m **\<^bsub>m\<^esub> x **\<^bsub>m\<^esub> y **\<^bsub>m\<^esub> l),
        n **\<^bsub>m\<^esub> (6 mod m **\<^bsub>m\<^esub> x **\<^bsub>m\<^esub> y **\<^bsub>m\<^esub> l --\<^bsub>m\<^esub> n ^^^\<^bsub>m\<^esub> 2) --\<^bsub>m\<^esub>
        2 mod m **\<^bsub>m\<^esub> y ^^^\<^bsub>m\<^esub> 2 **\<^bsub>m\<^esub> l ^^^\<^bsub>m\<^esub> 2,
        l ^^^\<^bsub>m\<^esub> 3))"
 
 lemma mpdouble_eq_mpdouble_nz:
   "snd (snd p) \<noteq> 0 \<Longrightarrow> mpdouble_nz m a p = mpdouble m a p"
   by (auto simp add: mpdouble_def mpdouble_nz_def split: prod.split)
 
 locale ell_prime_field = residues_prime_gt2 +
   fixes   A B :: nat
   assumes AB_in_carrier[simp]: "A \<in> carrier R" "B \<in> carrier R"
   and     non_singular:        "(4 * A ^ 3 + 27 * B ^ 2) mod p \<noteq> 0"
 begin
 
 definition curve :: "int point monoid" where
   "curve =
   \<lparr> carrier = ({ P. on_curve A B P }),
     monoid.mult = add A,
     monoid.one = Infinity \<rparr>"
 
 lemma curve_simps:
   shows in_carrier_curve: "P \<in> carrier curve \<longleftrightarrow> on_curve A B P"
     and add_curve: "x \<otimes>\<^bsub>curve\<^esub> y = add A x y"
     and one_curve: "\<one>\<^bsub>curve\<^esub> = Infinity"
   by (simp_all add: curve_def)
 
 lemma
   assumes "Point x y \<in> carrier curve"
   shows    Point_in_carrierD1: "x \<in> carrier R"
   and      Point_in_carrierD2: "y \<in> carrier R"
   using assms by (auto simp: in_carrier_curve on_curve_def)
 
 text \<open>Just a few basic facts for casting a nat as an int.\<close>
 lemma nat_int_eq:   "a = b \<longleftrightarrow> int a = int b" by simp
 lemma nat_int_less: "a < b \<longleftrightarrow> int a < int b" by simp
 lemma nat_int_le:   "a \<le> b \<longleftrightarrow> int a \<le> int b" by simp
 
 lemma nonsingular_in_bf: "nonsingular A B"
   using non_singular
   unfolding nonsingular_def res_of_natural_eq res_of_integer_eq res_mult_eq
     res_add_eq res_pow_eq res_zero_eq nat_int_eq zmod_int
   by (simp add: mod_simps)
 
 sublocale curve: comm_group curve
   apply (intro comm_groupI)
   using nonsingular_in_bf
   apply (auto simp: curve_simps add_0_l add_0_r Units_def
                     add_assoc[of "int A" "int B" _ _ _, symmetric]
                     add_comm[of A B] opp_closed
               intro!: add_closed)
   apply (intro bexI[of _ "opp _"])
   apply (auto simp: add_opp curve_simps intro!: opp_closed)
   done
 
 lemma inv_curve: "x \<in> carrier curve \<Longrightarrow> inv\<^bsub>curve\<^esub> x = opp x"
   by (intro curve.inv_unique'[symmetric])
      (auto simp: curve_simps add_opp add_comm[of A B _ x] opp_closed)
 
 lemma curve_square_is_mult: "P [^]\<^bsub>curve\<^esub> (2::nat) = P \<otimes>\<^bsub>curve\<^esub> P"
   unfolding nat_pow_def apply (simp add: curve_def curve_simps)
   by (simp add: ell_field_axioms ell_field.add_0_l)
 
 lemma finite_curve[simp]: "finite (carrier curve)"
 proof (rule finite_subset)
   show "carrier curve \<subseteq> case_prod Point ` (carrier R \<times> carrier R) \<union> { Infinity }"
     by (auto simp: in_carrier_curve on_curve_def split: point.splits)
 qed auto
 
 lemma Point_ne_one[simp]: "Point x y \<noteq> \<one>\<^bsub>curve\<^esub>"  "\<one>\<^bsub>curve\<^esub> \<noteq> Point x y"
   by (simp_all add: one_curve)
 
 lemma odd_p: "odd p"
   using p_prime gt2 using prime_odd_nat by auto
 
 lemma mod_of_in_carrier: "x \<in> carrier R \<Longrightarrow> x mod int p = x"
   by (simp add: res_carrier_eq)
 
 lemma nz_in_carrier_gcd:
   assumes "x \<in> carrier R"  "x \<noteq> 0"
   shows   "gcd x (int p) = 1"
 proof -
   have "0 < x \<and> x < int p" using assms res_carrier_eq by auto
   then show ?thesis using p_prime by (simp add: p_coprime_right_int zdvd_not_zless)
 qed
 
 text \<open>xy_to_pnt is for implementations that use (0,0) to represent Infinity.  Below are
 many lemmas that relate pairs of ints and the point type.  Similarly, xyz_to_pnt is useful
 for implementations that use triples of integers to represent points on the curve in 
 projective form.\<close>
 definition xy_to_pnt :: "int \<times> int \<Rightarrow> int point" where
   "xy_to_pnt =
     (\<lambda>(x, y). if x mod int p = 0 \<and> y mod int p = 0 then Infinity else Point (x mod p) (y mod p))"
 
 lemma xy_to_pnt_eq:
   "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow>
     xy_to_pnt (x, y) = (if x = \<zero>\<^bsub>R\<^esub> \<and> y = \<zero>\<^bsub>R\<^esub> then \<one>\<^bsub>curve\<^esub> else Point x y)"
   by (simp add: xy_to_pnt_def mod_of_in_carrier one_curve res_zero_eq)
 
 lemma xy_to_pnt_Point:
   assumes "xy_to_pnt (x, y) = Point x' y'"
   shows   "x mod p = x' \<and> y mod p = y'"
 proof -
   have "x mod int p \<noteq> 0 \<or> y mod int p \<noteq> 0"
     using assms unfolding xy_to_pnt_def by force
   then have "xy_to_pnt (x, y) = Point (x mod p) (y mod p)"
     using assms unfolding xy_to_pnt_def by fastforce
   then show ?thesis using assms by simp
 qed
 
 lemma xy_to_pnt_Infinity:
   assumes "xy_to_pnt (x, y) = Infinity"
   shows   "x mod p = 0 \<and> y mod p = 0"
 proof -
   have "Infinity = (if x mod int p = 0 \<and> y mod int p = 0 then Infinity
                     else Point (x mod int p) (y mod int p))"
     using assms xy_to_pnt_def by force
   then show ?thesis by (metis (no_types) point.simps(3))
 qed
 
 definition xyz_to_pnt :: "int \<times> int \<times> int \<Rightarrow> int point" where
   "xyz_to_pnt = (\<lambda>(x, y, z). if z mod int p = 0 then Infinity
            else Point ((x mod int p) \<oslash>\<^bsub>R\<^esub> (z mod int p)) ((y mod int p) \<oslash>\<^bsub>R\<^esub> (z mod int p)))"
 
 lemma xyz_to_pnt_zero_z[simp]: "xyz_to_pnt (x, y, \<zero>\<^bsub>R\<^esub>) = \<one>\<^bsub>curve\<^esub>"
   by (simp add: xyz_to_pnt_def mod_of_in_carrier one_curve zero_cong)
 
 lemma xyz_to_pnt_zero[simp]: "xyz_to_pnt (x, y, 0) = Infinity"
   by (simp add: xyz_to_pnt_def res_zero_eq)
 
 lemma xyz_to_pnt_eq:
   "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> z \<in> carrier R \<Longrightarrow>
     xyz_to_pnt (x, y, z) = (if z = \<zero>\<^bsub>R\<^esub> then \<one>\<^bsub>curve\<^esub> else Point (x \<oslash>\<^bsub>R\<^esub> z) (y \<oslash>\<^bsub>R\<^esub> z))"
   using xyz_to_pnt_def mod_of_in_carrier res_zero_eq one_curve by simp
 
 lemma xyz_to_pnt_z_1:
   assumes [simp]: "x \<in> carrier R"  "y \<in> carrier R"
   shows "xyz_to_pnt (x, y, \<one>\<^bsub>R\<^esub>) = Point x y"
 proof -
   have "(1::int) \<in> carrier R" using res_carrier_eq gt2 by auto
   then show ?thesis 
      unfolding xyz_to_pnt_def using mod_of_in_carrier m_gt_one assms divide_1 res_one_eq by auto
 qed
 
 lemma xyz_to_pnt_eq_make_affine:
   "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> z \<in> carrier R \<Longrightarrow>
     xyz_to_pnt (x, y, z) = make_affine (x, y, z)"
   by (simp add: xyz_to_pnt_def make_affine_def mod_of_in_carrier res_zero_eq)
 
 lemma xyz_to_pnt_in_carrier_on_curvep:
   assumes [simp]: "x \<in> carrier R"  "y \<in> carrier R"  "z \<in> carrier R"
                   "xyz_to_pnt (x, y, z) \<in> carrier curve"
   shows   "on_curvep A B (x, y, z)"
 proof -
   have "on_curve A B (make_affine (x, y, z))"
     by (simp flip: xyz_to_pnt_eq_make_affine in_carrier_curve)
   then show ?thesis
     by (subst on_curvep_iff_on_curve) (simp_all add: in_carrierp_def)
 qed
 
 lemma xyz_to_pnt_scale[symmetric]:
   assumes [simp]: "x \<in> carrier R"  "y \<in> carrier R"  "z \<in> carrier R"  "c \<in> carrier R"  "c \<noteq> \<zero>\<^bsub>R\<^esub>"
   shows   "xyz_to_pnt (x, y, z) = xyz_to_pnt (x \<otimes>\<^bsub>R\<^esub> c, y \<otimes>\<^bsub>R\<^esub> c, z \<otimes>\<^bsub>R\<^esub> c)"
   by (simp add: xyz_to_pnt_eq)
 
 lemma xyz_to_pnt_scale'[symmetric]:
   assumes [simp]: "x \<in> carrier R"  "y \<in> carrier R"  "z \<in> carrier R"  "c \<in> carrier R"
       and zc:     "z \<noteq> \<zero>\<^bsub>R\<^esub> \<Longrightarrow> c \<noteq> \<zero>\<^bsub>R\<^esub>"
   shows           "xyz_to_pnt (x, y, z) = xyz_to_pnt (x \<otimes>\<^bsub>R\<^esub> c, y \<otimes>\<^bsub>R\<^esub> c, z \<otimes>\<^bsub>R\<^esub> c)"
 proof cases
   assume "z = \<zero>\<^bsub>R\<^esub>" then show ?thesis
     using assms by (simp add: xyz_to_pnt_eq in_carrierp_def)
 next
   assume "z \<noteq> \<zero>\<^bsub>R\<^esub>" with zc show ?thesis
     using assms by (simp add: xyz_to_pnt_scale in_carrierp_def)
 qed
 
 lemma xyz_to_pnt_mod:
   "xyz_to_pnt (x mod int p, y mod int p, z mod int p) = xyz_to_pnt (x, y, z)"
   by (simp add: mod_of_in_carrier xyz_to_pnt_def)
 
 lemma inv_xyz_to_pnt:
   "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> z \<in> carrier R \<Longrightarrow> xyz_to_pnt (x, y, z) \<in> carrier curve \<Longrightarrow>
     inv\<^bsub>curve\<^esub> (xyz_to_pnt (x, y, z)) = xyz_to_pnt (x, \<ominus> y, z)"
   unfolding inv_curve opp_def by (auto simp add: xyz_to_pnt_eq one_curve)
 
 lemma xyz_to_pnt_dbl:
   assumes [simp]: "x \<in> carrier R"  "y \<in> carrier R"  "z \<in> carrier R"
   shows "xyz_to_pnt (x, y, z) \<otimes>\<^bsub>curve\<^esub> xyz_to_pnt (x, y, z) =
     (let l = \<guillemotleft>2\<guillemotright> \<otimes> y \<otimes> z; m = \<guillemotleft>3\<guillemotright> \<otimes> x [^] (2::nat) \<oplus> A \<otimes> z [^] (2::nat) in
       xyz_to_pnt (
         l \<otimes> (m [^] (2::nat) \<ominus> \<guillemotleft>4\<guillemotright> \<otimes> x \<otimes> y \<otimes> l),
         m \<otimes> (\<guillemotleft>6\<guillemotright> \<otimes> x \<otimes> y \<otimes> l \<ominus> m [^] (2::nat)) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> y [^] (2::nat) \<otimes> l [^] (2::nat),
         l [^] (3::nat)))" (is "?l = ?r")
 proof -
   have "?l = make_affine (pdouble A (x, y, z))"
     by (simp add: pdouble_correct in_carrierp_def add_curve xyz_to_pnt_eq_make_affine)
   also have "\<dots> = ?r"
     by (simp add: pdouble_def Let_def one_curve xyz_to_pnt_eq_make_affine)
   finally show ?thesis .
 qed
 
 lemma xyz_to_pnt_square:
   assumes "x \<in> carrier R"  "y \<in> carrier R"  "z \<in> carrier R"
   shows "xyz_to_pnt (x, y, z) [^]\<^bsub>curve\<^esub> (2::nat) =
     (let l = \<guillemotleft>2\<guillemotright> \<otimes> y \<otimes> z; m = \<guillemotleft>3\<guillemotright> \<otimes> x [^] (2::nat) \<oplus> A \<otimes> z [^] (2::nat) in
       xyz_to_pnt (
         l \<otimes> (m [^] (2::nat) \<ominus> \<guillemotleft>4\<guillemotright> \<otimes> x \<otimes> y \<otimes> l),
         m \<otimes> (\<guillemotleft>6\<guillemotright> \<otimes> x \<otimes> y \<otimes> l \<ominus> m [^] (2::nat)) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> y [^] (2::nat) \<otimes> l [^] (2::nat),
         l [^] (3::nat)))" (is "?l = ?r")
   unfolding curve_square_is_mult by (rule xyz_to_pnt_dbl) fact+
 
 lemma xyz_to_pnt_add:
   assumes [simp]:   "x\<^sub>1 \<in> carrier R"  "y\<^sub>1 \<in> carrier R"  "z\<^sub>1 \<in> carrier R"
   assumes [simp]:   "x\<^sub>2 \<in> carrier R"  "y\<^sub>2 \<in> carrier R"  "z\<^sub>2 \<in> carrier R"
   assumes in_curve: "xyz_to_pnt (x\<^sub>1, y\<^sub>1, z\<^sub>1) \<in> carrier curve"
                     "xyz_to_pnt (x\<^sub>2, y\<^sub>2, z\<^sub>2) \<in> carrier curve"
   assumes ne:       "xyz_to_pnt (x\<^sub>1, y\<^sub>1, z\<^sub>1) \<noteq> xyz_to_pnt (x\<^sub>2, y\<^sub>2, z\<^sub>2)"
   and     [simp]:   "z\<^sub>1 \<noteq> \<zero>" "z\<^sub>2 \<noteq> \<zero>"
   shows   "xyz_to_pnt (x\<^sub>1, y\<^sub>1, z\<^sub>1) \<otimes>\<^bsub>curve\<^esub> xyz_to_pnt (x\<^sub>2, y\<^sub>2, z\<^sub>2) =
     (let d\<^sub>1 = x\<^sub>2 \<otimes> z\<^sub>1; d\<^sub>2 = x\<^sub>1 \<otimes> z\<^sub>2;
          l = d\<^sub>1 \<ominus> d\<^sub>2; m = y\<^sub>2 \<otimes> z\<^sub>1 \<ominus> y\<^sub>1 \<otimes> z\<^sub>2;
          h = m [^] (2::nat) \<otimes> z\<^sub>1 \<otimes> z\<^sub>2 \<ominus> (d\<^sub>1 \<oplus> d\<^sub>2) \<otimes> l [^] (2::nat)
     in xyz_to_pnt (l \<otimes> h, (d\<^sub>2 \<otimes> l [^] (2::nat) \<ominus> h) \<otimes> m \<ominus> l [^] (3::nat) \<otimes> y\<^sub>1 \<otimes> z\<^sub>2,
                    l [^] (3::nat) \<otimes> z\<^sub>1 \<otimes> z\<^sub>2))" (is "?l = ?r")
 proof -
   from ne have *: "\<not> (y\<^sub>2 \<otimes> z\<^sub>1 = y\<^sub>1 \<otimes> z\<^sub>2 \<and> x\<^sub>2 \<otimes> z\<^sub>1 = x\<^sub>1 \<otimes> z\<^sub>2)"
     by (auto simp add: xyz_to_pnt_eq simp flip: mult_eq_iff_eq_divide eq_mult_iff_divide_eq)
 
   have "?l = make_affine (padd A (x\<^sub>1, y\<^sub>1, z\<^sub>1) (x\<^sub>2, y\<^sub>2, z\<^sub>2))"
     using in_curve
     by (simp add: padd_correct[where b=B] in_carrierp_def curve_simps
                   xyz_to_pnt_eq_make_affine on_curvep_iff_on_curve)
   also have "\<dots> = ?r"
     using *
     by (auto simp add: padd_def Let_def xyz_to_pnt_eq_make_affine
                 simp flip: one_curve)
   finally show ?thesis .
 qed
 
 lemma xyz_to_pnt_padd:
   assumes [simp]:   "x\<^sub>1 \<in> carrier R"  "y\<^sub>1 \<in> carrier R"  "z\<^sub>1 \<in> carrier R"
   assumes [simp]:   "x\<^sub>2 \<in> carrier R"  "y\<^sub>2 \<in> carrier R"  "z\<^sub>2 \<in> carrier R"
   assumes in_curve: "xyz_to_pnt (x\<^sub>1, y\<^sub>1, z\<^sub>1) \<in> carrier curve"
                     "xyz_to_pnt (x\<^sub>2, y\<^sub>2, z\<^sub>2) \<in> carrier curve"
   shows   "xyz_to_pnt (padd A (x\<^sub>1, y\<^sub>1, z\<^sub>1) (x\<^sub>2, y\<^sub>2, z\<^sub>2)) =
            xyz_to_pnt (x\<^sub>1, y\<^sub>1, z\<^sub>1) \<otimes>\<^bsub>curve\<^esub> xyz_to_pnt (x\<^sub>2, y\<^sub>2, z\<^sub>2)"
   apply (subst (1 2) xyz_to_pnt_eq_make_affine)
   apply (simp_all add: curve_simps)
   apply (subst padd_correct[symmetric, OF AB_in_carrier])
   using in_curve
   apply (simp_all add: xyz_to_pnt_eq_make_affine padd_def pdouble_def Let_def curve_simps
       on_curvep_iff_on_curve in_carrierp_def)
   done
 
 lemma Point_Point_eq_one_iff:
   assumes 1: "Point x1 y1 \<in> carrier curve"
   and     2: "Point x2 y2 \<in> carrier curve"
   shows "Point x1 y1 \<otimes>\<^bsub>curve\<^esub> Point x2 y2 = \<one>\<^bsub>curve\<^esub> \<longleftrightarrow> (x1 = x2 \<and> y1 = \<ominus> y2)"
   by (subst curve.m_one_iff[OF 1 2]) (simp add: inv_curve 1 2 opp_def)
 
 lemma y_coord_eq_or_eq_neg:
   "Point x y1 \<in> carrier curve \<Longrightarrow> Point x y2 \<in> carrier curve \<Longrightarrow> y1 = y2 \<or> y1 = \<ominus> y2"
   by (auto simp: in_carrier_curve on_curve_def eq_commute[of _ "_  \<oplus> _"] power2_eq_square
                  square_eq_iff)
 
 lemma yz_coord_eq_or_eq_neg:
   assumes [simp]:
     "x \<in> carrier R"  "y1 \<in> carrier R"  "y2 \<in> carrier R"  "z \<in> carrier R"
   shows "xyz_to_pnt (x, y1, z) \<in> carrier curve \<Longrightarrow>
          xyz_to_pnt (x, y2, z) \<in> carrier curve \<Longrightarrow> z \<noteq> \<zero>\<^bsub>R\<^esub> \<Longrightarrow> y1 = y2 \<or> y1 = \<ominus> y2"
   using y_coord_eq_or_eq_neg[of "x \<oslash> z" "y1 \<oslash> z" "y2 \<oslash> z"]
   by (auto simp add: xyz_to_pnt_eq div_cancel)
 
 lemma xyz_coord_eq_or_eq_neg:
   assumes [simp]: "x1 \<in> carrier R"  "y1 \<in> carrier R"  "z1 \<in> carrier R"
                   "x2 \<in> carrier R"  "y2 \<in> carrier R"  "z2 \<in> carrier R"
   assumes 1:      "xyz_to_pnt (x1, y1, z1) \<in> carrier curve"
   assumes 2:      "xyz_to_pnt (x2, y2, z2) \<in> carrier curve"
   and     [simp]: "z1 \<noteq> \<zero>"  "z2 \<noteq> \<zero>"
   and     x: "x1 \<otimes> z2 = x2 \<otimes> z1"
   shows "y1 \<otimes> z2 = y2 \<otimes> z1 \<or> y1 \<otimes> z2 = \<ominus> y2 \<otimes> z1"
   apply (subst (1 2) divide_eq_divide_iff_mult_eq_mult[symmetric])
   apply (simp_all flip: minus_divide_left)
   using 1 2 x y_coord_eq_or_eq_neg[of "x1 \<oslash> z1" "y1 \<oslash> z1" "y2 \<oslash> z2"]
   apply (subst (asm) divide_eq_divide_iff_mult_eq_mult[symmetric])
   apply (auto simp: xyz_to_pnt_eq split: if_splits)
   done
 
 end (* of ell_prime_field locale *)
 
 section \<open>Added for SEC1\<close>
 text \<open>This section adds more facts about an elliptic curve as a group.  For example, we examine
 the order of points on the curve and the order of the curve itself.\<close>
 
 context ell_prime_field
 begin
 
 lemma multEqPowInCurve:
   assumes "on_curve A B P" 
   shows   "point_mult A x P = P [^]\<^bsub>curve\<^esub> x"
 proof (induct x)
   case 0
   then show ?case by (simp add: one_curve) 
 next
   case (Suc x)
   then show ?case
     using add_curve curve.nat_pow_Suc2 in_carrier_curve assms point_mult.simps(2) 
     by presburger 
 qed
 
 text \<open>If P is not the point at infinity, n is a prime, and nP = the point at infinity, then
 n is actually the order of P.  So if 0 < x < n, xP \<noteq> the point at infinity.\<close>
 lemma order_n: 
   assumes "x < n"  "0 < x"  "on_curve A B P"  "P \<noteq> Infinity"  "point_mult A n P = Infinity" 
           "prime (n::nat)"
   shows   "point_mult A x P \<noteq> Infinity"
 proof - 
   have 1: "gcd n x = 1" 
     by (metis assms(1,2,6) gcd_dvd1 gcd_le2_nat neq0_conv not_le prime_nat_iff) 
   obtain i and j where 2: "i*(int n) + j*(int x) = 1" 
     by (metis bezw_aux 1 int_ops(2))
   have 3: "P = P [^]\<^bsub>curve\<^esub>(i*(int n) + j*(int x))"  
     by (simp add: 2 assms(3) in_carrier_curve) 
   have 4: "P = P [^]\<^bsub>curve\<^esub>(i*(int n)) \<otimes>\<^bsub>curve\<^esub> P [^]\<^bsub>curve\<^esub>(j*(int x))"
     using assms(3) in_carrier_curve 3 curve.int_pow_mult by auto
   have 5: "P = (P [^]\<^bsub>curve\<^esub>(int n))[^]\<^bsub>curve\<^esub>i \<otimes>\<^bsub>curve\<^esub> 
                (P [^]\<^bsub>curve\<^esub>(int x))[^]\<^bsub>curve\<^esub>j"
     by (metis assms(3) in_carrier_curve 4 curve.int_pow_pow mult_of_nat_commute)
   have 6: "P = (P [^]\<^bsub>curve\<^esub>(int x))[^]\<^bsub>curve\<^esub>j" 
     by (metis assms(3,5) in_carrier_curve 5 curve.int_pow_closed curve.int_pow_one one_curve
               curve.l_one int_pow_int multEqPowInCurve) 
   have 7: "P [^]\<^bsub>curve\<^esub> x = \<one>\<^bsub>curve\<^esub> \<longrightarrow> P = \<one>\<^bsub>curve\<^esub>"
     by (metis 6 curve.int_pow_one int_pow_int) 
   show ?thesis 
     using assms(3,4) 7 one_curve multEqPowInCurve by auto 
 qed
 
 lemma order_n': 
   assumes "x < n"  "0 < x"  "on_curve A B P"  "P \<noteq> Infinity"  "point_mult A n P = Infinity"
           "prime (n::nat)"
   shows   "P [^]\<^bsub>curve\<^esub> x \<noteq> \<one>\<^bsub>curve\<^esub>"
   using assms order_n one_curve multEqPowInCurve in_carrier_curve by algebra
 
 text \<open>The idea for the next two lemmas is that every point on the cycle of order n are the "same."
 So if you start at one point on the cycle (not Infinity), then you can get to any other point on
 the cycle by multiplying by some scalar x.  Then the point you land on will also be on the curve,
 have order n, and not be infinity (as long as n does not divide x.)\<close>
 lemma order_n_cycle:
   assumes "on_curve A B P"  "point_mult A n P = Infinity"  "Q = point_mult A x P"
   shows   "point_mult A n Q = Infinity"
   by (metis AB_in_carrier(1,2) assms(1,2,3) curve.int_pow_one curve.int_pow_pow curve_simps(1) 
             int_pow_int mult.commute multEqPowInCurve one_curve point_mult_closed)
 
 lemma order_n_cycle':
   assumes "x < n"  "0 < x"  "on_curve A B P"  "P \<noteq> Infinity"  "point_mult A n P = Infinity" 
           "prime (n::nat)"  "Q = point_mult A x P" 
   shows   "on_curve A B Q \<and> Q \<noteq> Infinity \<and> point_mult A n Q = Infinity"
   using AB_in_carrier(1,2) assms order_n order_n_cycle point_mult_closed 
   by presburger
 
 lemma multQmodn:
   assumes "on_curve A B Q"  "point_mult A n Q = Infinity" 
   shows   "point_mult A x Q = point_mult A (x mod n) Q"
 proof - 
   let ?d = "x div n"
   let ?m = "x mod n"
   have 1: "x = ?d*n + ?m"  using div_mod_decomp by blast 
   have 2: "point_mult A x Q = Q [^]\<^bsub>curve\<^esub> (?d*n + ?m)"
     using in_carrier_curve assms(1) multEqPowInCurve by presburger 
   have 3: "Q [^]\<^bsub>curve\<^esub> (?d*n + ?m) = Q [^]\<^bsub>curve\<^esub>(?d*n)\<otimes>\<^bsub>curve\<^esub>Q [^]\<^bsub>curve\<^esub>?m"
     using curve.nat_pow_mult assms(1) in_carrier_curve by presburger
   have 4: "Q [^]\<^bsub>curve\<^esub>(?d*n) = (Q [^]\<^bsub>curve\<^esub>n)[^]\<^bsub>curve\<^esub>?d" 
     by (simp add: curve.nat_pow_pow assms(1) in_carrier_curve mult.commute) 
   have 5: "Q [^]\<^bsub>curve\<^esub>(?d*n) = \<one>\<^bsub>curve\<^esub>" 
     using 4 assms(1,2) curve.nat_pow_one one_curve multEqPowInCurve by algebra
   show ?thesis 
     using 3 5 multEqPowInCurve curve.nat_pow_closed in_carrier_curve assms(1) by force
 qed
 
 lemma multQmodn':
   assumes "on_curve A B Q"  "point_mult A n Q = Infinity" 
   shows   "Q[^]\<^bsub>curve\<^esub>x = Q[^]\<^bsub>curve\<^esub>(x mod n)"
   by (metis assms(1,2) multEqPowInCurve multQmodn)
 
 lemma multQmodn'int_pos:
   assumes "on_curve A B Q"  "point_mult A n Q = Infinity"  "0 \<le> (x::int)"
   shows   "Q[^]\<^bsub>curve\<^esub>x = Q[^]\<^bsub>curve\<^esub>(x mod n)"
   by (metis assms int_pow_int multQmodn' zero_le_imp_eq_int zmod_int)
 
 lemma multQmodn'int_neg: 
   assumes "on_curve A B Q"  "point_mult A n Q = Infinity"  "(x::int) < 0"  "1 < n"
   shows   "Q[^]\<^bsub>curve\<^esub>(x::int) = Q[^]\<^bsub>curve\<^esub>(x mod n)"
 proof - 
   let ?y = "-x"
   have 1: "Q[^]\<^bsub>curve\<^esub>(?y*n) = \<one>\<^bsub>curve\<^esub>" 
     by (metis assms(1,2) curve.int_pow_one curve.int_pow_pow one_curve int_pow_int 
               multEqPowInCurve mult_of_nat_commute in_carrier_curve) 
   have 2: "0 \<le> x + ?y*n" 
     using assms(3,4) by auto
   have 3: "x mod n = (x + ?y*n) mod n" 
     by presburger 
   have 4: "Q[^]\<^bsub>curve\<^esub>(x + ?y*n) = Q[^]\<^bsub>curve\<^esub>((x + ?y*n) mod n)" 
     using 2 assms(1,2) multQmodn'int_pos by fast
   have 5: "Q[^]\<^bsub>curve\<^esub>(x + ?y*n) = Q[^]\<^bsub>curve\<^esub>x \<otimes>\<^bsub>curve\<^esub> Q[^]\<^bsub>curve\<^esub>(?y*n)"
     using curve.int_pow_mult assms(1) in_carrier_curve by presburger
   have 6: "Q[^]\<^bsub>curve\<^esub>(x + ?y*n) = Q[^]\<^bsub>curve\<^esub>x"
     using 1 5 assms(1) in_carrier_curve by force
   show ?thesis using 3 4 6 by argo
 qed
 
 lemma multQmodn'int: 
   assumes "on_curve A B Q"  "point_mult A n Q = Infinity"  "1 < n"
   shows   "Q[^]\<^bsub>curve\<^esub>(x::int) = Q[^]\<^bsub>curve\<^esub>(x mod n)"
   apply (cases "0 \<le> x")
   using assms(1,2)   multQmodn'int_pos apply fast
   using assms(1,2,3) multQmodn'int_neg by simp
 
 
 text \<open>We use the above to relate to the definition of "ord" for a group.\<close>
 lemma curve_ord_n1: 
   assumes "on_curve A B P"  "point_mult A n P = Infinity"  "n dvd x"
   shows   "point_mult A x P = Infinity"
   by (metis assms(1,2,3) dvd_eq_mod_eq_0 multQmodn point_mult.simps(1))
 
 lemma curve_ord_n2: 
   assumes "on_curve A B P"  "P \<noteq> Infinity"  "point_mult A n P = Infinity" 
           "prime (n::nat)"  "\<not> n dvd x"
   shows   "point_mult A x P \<noteq> Infinity"
 proof - 
   let ?m = "x mod n"
   have "0 < ?m \<and> ?m < n" 
     by (simp add: assms(4,5) mod_greater_zero_iff_not_dvd prime_gt_0_nat) 
   then show ?thesis by (metis assms(1,2,3,4) order_n multQmodn)
 qed
 
 lemma curve_ord_n3: 
   assumes "on_curve A B P"  "P \<noteq> Infinity"  "point_mult A n P = Infinity"  "prime (n::nat)" 
   shows   "(n dvd x) = (point_mult A x P = Infinity)"
   by (meson assms(1,2,3,4) curve_ord_n1 curve_ord_n2)
 
 lemma curve_ord_n4: 
   assumes "on_curve A B P"  "P \<noteq> Infinity"  "point_mult A n P = Infinity"  "prime (n::nat)" 
   shows   "(n dvd x) = (P[^]\<^bsub>curve\<^esub>x = \<one>\<^bsub>curve\<^esub>)"
   using assms curve_ord_n3 multEqPowInCurve one_curve by presburger
 
 lemma curve_ord_n5: 
   assumes "on_curve A B P"  "P \<noteq> Infinity"  "point_mult A n P = Infinity"  "prime (n::nat)" 
   shows   "curve.ord P = n"
   using assms curve_ord_n4 curve.ord_def curve.ord_unique in_carrier_curve by presburger
 
 lemma curve_ord_n6: 
   assumes "on_curve A B P"  "P \<noteq> \<one>\<^bsub>curve\<^esub>"  "point_mult A n P = \<one>\<^bsub>curve\<^esub>"  "prime (n::nat)" 
           "d1 < n"  "d2 < n"  "d1 < d2" 
   shows   "P [^]\<^bsub>curve\<^esub> d1 \<noteq> P [^]\<^bsub>curve\<^esub> d2"
 proof - 
   let ?d = "d2 - d1"
   have d1: "0 < ?d \<and> ?d < n"  using assms(5,6,7) by linarith
   have d2: "\<not> n dvd ?d"       using d1 by auto
   have A1: "(P [^]\<^bsub>curve\<^esub> d1 = P [^]\<^bsub>curve\<^esub> d2) \<longrightarrow> P [^]\<^bsub>curve\<^esub> ?d = \<one>\<^bsub>curve\<^esub>" 
     using assms(1) curve.pow_eq_div2 curve_simps(1) by presburger
   show ?thesis by (metis d2 A1 assms(1,2,3,4) curve_ord_n4 curve_simps(3)) 
 qed
 
 lemma curve_ord_n7: 
   assumes "on_curve A B P"  "P \<noteq> \<one>\<^bsub>curve\<^esub>"  "point_mult A n P = \<one>\<^bsub>curve\<^esub>"  "prime (n::nat)" 
           "d1 < n"  "d2 < n"  "d1 \<noteq> d2" 
   shows   "P [^]\<^bsub>curve\<^esub> d1 \<noteq> P [^]\<^bsub>curve\<^esub> d2"
   apply (cases "d1 < d2") 
   using assms curve_ord_n6 apply blast 
   by (metis assms curve_ord_n6 verit_comp_simplify(3) verit_la_disequality) 
 
 lemma curve_cycle_n1:
   assumes "on_curve A B P"  "P \<noteq> \<one>\<^bsub>curve\<^esub>"  "point_mult A n P = \<one>\<^bsub>curve\<^esub>"  "prime (n::nat)" 
   shows   "card {Q. (\<exists>d<n. Q = P [^]\<^bsub>curve\<^esub> d)} = n"
 proof - 
   let ?S1 = "{d. d<n}"
   let ?S2 = "{Q. (\<exists>d<n. Q = P [^]\<^bsub>curve\<^esub> d)}"
   have 1: "card ?S1 = n"        by force
   let ?f = "\<lambda>d. P [^]\<^bsub>curve\<^esub> d"
   have 2: "inj_on ?f ?S1" 
     by (metis (mono_tags, lifting) assms curve_ord_n7 inj_on_def mem_Collect_eq)
   have 3: "?f ` ?S1 = ?S2"      by blast
   have 4: "bij_betw ?f ?S1 ?S2" by (simp add: 2 3 bij_betw_def) 
   show ?thesis                  using 1 4 bij_betw_same_card by force  
 qed
 
 lemma curve_cycle_n2:
   assumes "on_curve A B P"  "P \<noteq> Infinity"  "point_mult A n P = Infinity"  "prime (n::nat)" 
   shows   "card {Q. (\<exists>d<n. Q = point_mult A d P)} = n"
   using assms curve_cycle_n1 multEqPowInCurve one_curve by presburger 
 
 end (* of ell_prime_field context *)
 
 section \<open>Additions to Elliptic_test\<close>
 
 text \<open>Elliptic_Test only defines addition and scalar multiplication for integer points that are
 in projective form.  We want to have these defined for affine (integer) points.  This becomes
 important when we are running test vectors.\<close>
 
 context residues_prime_gt2
 begin
 
 definition point_madd :: "nat \<Rightarrow> int point \<Rightarrow> int point \<Rightarrow> int point" where
   "point_madd a p\<^sub>1 p\<^sub>2 = (case p\<^sub>1 of
        Infinity \<Rightarrow> p\<^sub>2
      | Point x\<^sub>1 y\<^sub>1 \<Rightarrow> (case p\<^sub>2 of
          Infinity \<Rightarrow> p\<^sub>1
        | Point x\<^sub>2 y\<^sub>2 \<Rightarrow>
            if x\<^sub>1 = x\<^sub>2 then
              if (y\<^sub>1 = - y\<^sub>2 mod (int p)) then Infinity
              else
                let
                  twoy1   = nat ((2*y\<^sub>1) mod (int p));
                  inv_2y1 = int (inv_mod p twoy1);
                  l       = ((3 * x\<^sub>1^2 + (int a)) * inv_2y1) mod p;
                  x\<^sub>3 = (l^2 - 2*x\<^sub>1) mod (int p);
                  y\<^sub>3 = (- y\<^sub>1 - l * (x\<^sub>3 - x\<^sub>1)) mod (int p)
                in
                  Point x\<^sub>3 y\<^sub>3
            else
              let
                x2_x1     = nat ((x\<^sub>2 - x\<^sub>1) mod (int p));
                inv_x2_x1 = int (inv_mod p x2_x1);
                l = ((y\<^sub>2 - y\<^sub>1) * inv_x2_x1) mod (int p);
                x\<^sub>3 = (l^2 - x\<^sub>1 - x\<^sub>2) mod (int p);
                y\<^sub>3 = (- y\<^sub>1 - l * (x\<^sub>3 - x\<^sub>1)) mod (int p)
              in
                Point x\<^sub>3 y\<^sub>3 ) )"
 
 fun point_mmult :: "nat \<Rightarrow> nat \<Rightarrow> int point \<Rightarrow> int point" where
     "point_mmult a 0 P = Infinity"
   | "point_mmult a (Suc n) P = point_madd a P (point_mmult a n P)"
 
 lemma add_eq_h1:
   assumes  "p\<^sub>1 = Point x1 y1" "p\<^sub>2 = Point x2 y2" "x1 = x2" "y1 \<noteq> \<ominus>\<^bsub>R\<^esub> y2"
            "l = (\<guillemotleft>3\<guillemotright> \<otimes>\<^bsub>R\<^esub> x1 [^] (2::nat) \<oplus>\<^bsub>R\<^esub> a) \<oslash>\<^bsub>R\<^esub> (\<guillemotleft>2\<guillemotright> \<otimes>\<^bsub>R\<^esub> y1)"
            "x3 = l [^] (2::nat) \<ominus>\<^bsub>R\<^esub> \<guillemotleft>2\<guillemotright> \<otimes>\<^bsub>R\<^esub> x1" "y3 = (\<ominus>\<^bsub>R\<^esub> y1 \<ominus>\<^bsub>R\<^esub> l \<otimes>\<^bsub>R\<^esub> (x3 \<ominus>\<^bsub>R\<^esub> x1))"
   shows    "add a p\<^sub>1 p\<^sub>2 = Point x3 y3"
   unfolding add_def Let_def using assms point.distinct
   by simp 
 
 lemma add_eq_h2: 
   assumes  "p\<^sub>1 = Point x1 y1" "p\<^sub>2 = Point x2 y2" "x1 = x2" "(y1 \<noteq> - y2 mod (int p))" 
            "twoy1 = nat ((2*y1) mod (int p))" "inv_2y1 = int (inv_mod p twoy1)"
            "l = ((3 * x1^2 + (int a)) * inv_2y1) mod p" "x3 = (l^2 - 2*x1) mod (int p)"
            "y3 = (- y1 - l * (x3 - x1)) mod (int p)"
          shows    "point_madd a p\<^sub>1 p\<^sub>2 = Point x3 y3"
   by (simp add: assms(1-2) assms(4) assms(8-9) point_madd_def Let_def
     flip: assms(3) assms(5) assms(6) assms(7))
 
 lemma point_add_eq [code]: "add a p\<^sub>1 p\<^sub>2 = point_madd a p\<^sub>1 p\<^sub>2"
 proof (cases p\<^sub>1)
   case Infinity
   then show ?thesis by (simp add: point_madd_def add_0_l) 
 next
   case P1: (Point x1 y1)
   show ?thesis proof (cases p\<^sub>2)
     case Infinity
     then show ?thesis using P1 point_madd_def add_0_r by auto 
   next
     case P2: (Point x2 y2)
     then show ?thesis proof (cases "x1 = x2")
       case x_eq: True
       then show ?thesis proof (cases "y1 = \<ominus>\<^bsub>R\<^esub> y2")
         case y_neg: True
         have A1: "(y1 = - y2 mod (int p))"        using res_neg_eq y_neg by blast 
         have A2:        "add a p\<^sub>1 p\<^sub>2 = Infinity"   using add_def P1 P2 x_eq y_neg by fastforce
         have A3: "point_madd a p\<^sub>1 p\<^sub>2 = Infinity"   using point_madd_def P1 P2 x_eq A1 by force
         show ?thesis                              using A2 A3 by presburger 
       next
         case y_nneg: False
         have B0: "(y1 \<noteq> - y2 mod (int p))"        using y_nneg res_neg_eq by algebra
         let ?twoy1   = "((2*y1) mod (int p))"
         let ?inv_2y1 = "int (inv_mod p (nat ?twoy1))"
         let ?l       = "((3 * x1^2 + (int a)) * ?inv_2y1) mod p"
         let ?l'      = "(\<guillemotleft>3\<guillemotright> \<otimes>\<^bsub>R\<^esub> x1 [^] (2::nat) \<oplus>\<^bsub>R\<^esub> a) \<oslash>\<^bsub>R\<^esub> (\<guillemotleft>2\<guillemotright> \<otimes>\<^bsub>R\<^esub> y1)"
         have B1: "\<guillemotleft>2\<guillemotright> \<otimes>\<^bsub>R\<^esub> y1 = (2*y1) mod (int p)"
           by (simp add: mod_mult_right_eq mult.commute res_mult_eq res_of_integer_eq)
         have B2: "0 \<le> (2*y1) mod (int p)"
           using gt2 by auto
         have B3: "(\<guillemotleft>3\<guillemotright> \<otimes>\<^bsub>R\<^esub> x1 [^] (2::nat) \<oplus>\<^bsub>R\<^esub> a) = (3 * x1^2 + (int a)) mod p"
           by (metis mod_mod_trivial res_add_eq local.of_int_add local.of_int_mult 
                     res_of_integer_eq res_pow_eq)
         have B4: "?inv_2y1 mod p = ?inv_2y1"
           by (metis inv_mod_def mod_mod_trivial zmod_int) 
         have B5: "?l = (((3 * x1^2 + (int a)) mod p) * ?inv_2y1) mod p" 
           by (metis mod_mult_left_eq) 
         have B6: "?l = ((3 * x1^2 + (int a)) mod p) \<oslash>\<^bsub>R\<^esub> ?twoy1" 
           by (smt (verit, ccfv_SIG) B2 B4 R_def cring_class.of_nat_0 gt2 int_distrib(4) 
               int_nat_eq inv_mod_0' m_div_def m_gt_one mod_in_carrier nat_int of_nat_0_less_iff 
               res_to_cong_simps(2) res_zero_eq residues_prime.inv_mod_p_inv_in_ring 
               residues_prime.p_prime residues_prime_axioms) 
         have B7: "?l = (\<guillemotleft>3\<guillemotright> \<otimes>\<^bsub>R\<^esub> x1 [^] (2::nat) \<oplus>\<^bsub>R\<^esub> a) \<oslash>\<^bsub>R\<^esub> ?twoy1" using B6 B3 by argo
         have B8: "?l = ?l'" using B7 B1 by argo
         let ?x3  = "(?l^2 - 2*x1) mod (int p)"
         let ?x3' = "?l' [^] (2::nat) \<ominus>\<^bsub>R\<^esub> \<guillemotleft>2\<guillemotright> \<otimes>\<^bsub>R\<^esub> x1"
         have B9: "?x3 = ?x3'" 
           by (metis B8 of_int_diff mod_mult_left_eq res_mult_eq res_of_integer_eq res_pow_eq)
         let ?y3  = "(- y1 - ?l * (?x3 - x1)) mod (int p)"
         let ?y3' = "(\<ominus>\<^bsub>R\<^esub> y1 \<ominus>\<^bsub>R\<^esub> ?l' \<otimes>\<^bsub>R\<^esub> (?x3 \<ominus>\<^bsub>R\<^esub> x1))"
         have B10: "?y3 = ?y3'" 
           by (smt (verit) B8 B9 mod_diff_eq mod_mod_trivial mult_cong res_diff_eq res_neg_eq) 
         have B11: "add a p\<^sub>1 p\<^sub>2 = Point ?x3 ?y3"  
           using y_nneg add_eq_h1 B9 B10 P1 P2 x_eq by blast
         have B12: "point_madd a p\<^sub>1 p\<^sub>2 = Point ?x3 ?y3" 
           using B0 add_eq_h2 B9 B10 P1 P2 x_eq by algebra
         show ?thesis using B11 B12 by argo 
       qed
     next
       case x_neq: False
       let ?x2_x1     = "((x2 - x1) mod (int p))"
       let ?inv_x2_x1 = "int (inv_mod p (nat ?x2_x1))"
       let ?l  = "((y2 - y1) * ?inv_x2_x1) mod (int p)"
       let ?x3 = "(?l^2 - x1 - x2) mod (int p)"
       let ?y3 = "(- y1 - ?l * (?x3 - x1)) mod (int p)"
       have C1: "point_madd a p\<^sub>1 p\<^sub>2 = Point ?x3 ?y3" 
         unfolding point_madd_def Let_def using x_neq P1 P2 by auto
       let ?l'  = "(y2 \<ominus>\<^bsub>R\<^esub> y1) \<oslash>\<^bsub>R\<^esub> (x2 \<ominus>\<^bsub>R\<^esub> x1)"
       let ?x3' = "?l' [^] (2::nat) \<ominus>\<^bsub>R\<^esub> x1 \<ominus>\<^bsub>R\<^esub> x2"
       let ?y3' = "(\<ominus>\<^bsub>R\<^esub> y1 \<ominus>\<^bsub>R\<^esub> ?l' \<otimes>\<^bsub>R\<^esub> (?x3' \<ominus>\<^bsub>R\<^esub> x1))"
       have C2: "add a p\<^sub>1 p\<^sub>2 = Point ?x3' ?y3'" 
         unfolding add_def Let_def using x_neq P1 P2 by auto
       have C3: "?l = ?l'"
         by (smt (verit, ccfv_threshold) Euclidean_Rings.pos_mod_sign R_m_def gt2
         int_nat_eq int_ops(1) integral_iff inv_mod_0' m_div_def mod_in_carrier mod_mod_trivial 
         mult_cong nat_int nat_less_iff res_diff_eq residues.res_mult_eq residues_axioms zero_cong
         residues_prime.inv_mod_p_inv_in_ring residues_prime.p_prime residues_prime_axioms)
       have C4: "?x3 = ?x3'" 
         by (simp add: C3 mod_diff_left_eq res_diff_eq res_pow_eq) 
       have C5: "?y3 = ?y3'" 
         by (smt (verit) C3 C4 mod_diff_eq mod_mod_trivial mult_cong res_diff_eq res_neg_eq) 
       show ?thesis using C1 C2 C4 C5 by argo
     qed 
   qed
 qed
 
 lemma point_mult_eq [code]: "point_mult a n P = point_mmult a n P"
   apply (induct n) apply simp using point_add_eq by force
 
 text \<open>Also in Elliptic_Test, they provide methods for converting a point in projective coordinates
 to a point in affine coordinates, but not the other way around.  Here we provide a few more tools
 for going between affine and projective coordinates.\<close>
 
 definition get_x :: "int point \<Rightarrow> int" where
   "get_x P = (case P of
       Infinity  \<Rightarrow> 0
     | Point x y \<Rightarrow> x)"
 
 definition get_y :: "int point \<Rightarrow> int" where
   "get_y P = (case P of
       Infinity  \<Rightarrow> 0
     | Point x y \<Rightarrow> y)"
 
 lemma get_coords_correct:
   assumes "P = Point x y"
   shows   "P = Point (get_x P) (get_y P)"
   by (simp add: assms get_x_def get_y_def)
 
 definition mmake_proj :: "int point \<Rightarrow> int ppoint" where
   "mmake_proj P = (if P = Infinity then (1,1,0) else (get_x P, get_y P, 1))"
 
 lemma bezout_coeff_1: 
   assumes "1 < (x::nat)" 
   shows   "bezout_coefficients 1 x = (1,0)"
 proof - 
   have 10: "1 div x = 0"  using assms(1) by fastforce 
   have 11: "x \<noteq> 0"        using assms(1) by fastforce
   have 12: "euclid_ext_aux 1 0 0 1 1 x = euclid_ext_aux 0 (1 - 0 * 0) 1 (0 - 0 * 1) x (1 mod x)"
     by (smt (verit, ccfv_threshold) 10 11 euclid_ext_aux.simps mult_cancel_left1 of_nat_1 
-        of_nat_eq_0_iff of_nat_mod unique_euclidean_semiring_with_nat_class.of_nat_div) 
+        of_nat_eq_0_iff of_nat_mod linordered_euclidean_semiring_class.of_nat_div) 
   have 1: "euclid_ext_aux 1 0 0 1 1 x = euclid_ext_aux 0 1 1 0 x 1"
     using 12 assms(1) by force
   have 20: "x div 1 = x"  by simp
   have 21: "(1::int) \<noteq> 0" by simp
   have 22: "euclid_ext_aux 0 1 1 0 x 1 = euclid_ext_aux 1 (0 - x * 1) 0 (1 - x * 0) 1 (x mod 1)"
     by (smt (verit, ccfv_threshold)20 21 euclid_ext_aux.simps mult_cancel_left1 of_nat_1 
-        of_nat_eq_0_iff of_nat_mod unique_euclidean_semiring_with_nat_class.of_nat_div mod_by_1)
+        of_nat_eq_0_iff of_nat_mod linordered_euclidean_semiring_class.of_nat_div mod_by_1)
   have 2:  "euclid_ext_aux 0 1 1 0 x 1 = euclid_ext_aux 1 (0 - x) 0 1 1 0" 
     using 22 assms(1) by simp
   have 3: "euclid_ext_aux 1 (0 - x) 0 1 1 0 = ((1,0), 1)"
     by (metis (no_types, lifting) euclid_ext_aux.simps div_by_1 mult_1 mult_eq_0_iff 
         normalize_div unit_factor_1) 
   have 4: "euclid_ext 1 x = ((1,0), 1)"
     using 1 2 3 by presburger
   show ?thesis using 4 by simp
 qed
 
 lemma to_proj_to_aff: 
   assumes "0 \<le> get_x P" "get_x P < p" "0 \<le> get_y P" "get_y P < p" 
   shows   "mmake_affine (int p) (mmake_proj P) = P"
 proof (cases P)
   case Infinity
   then show ?thesis using mmake_proj_def mmake_affine_def by simp
 next
   case C: (Point x y)
   have Cx: "x = get_x P"            by (simp add: C get_x_def)
   have Cy: "y = get_y P"            by (simp add: C get_y_def)
   have C1: "mmake_proj P = (x,y,1)" using C Cx Cy mmake_proj_def by fastforce
   have C2: "bezout_coefficients 1 (int p) = (1,0)" using bezout_coeff_1 m_gt_one by fastforce 
   have C3: "1 **\<^bsub>(int p)\<^esub> x = x"    using assms(1,2) mmult_def Cx by simp
   have C4: "1 **\<^bsub>(int p)\<^esub> y = y"    using assms(3,4) mmult_def Cy by simp
   have C5: "mmake_affine (int p) (x,y,1) = Point x y"  using mmake_affine_def C2 C3 C4 by force
   show ?thesis                      using C C1 C5 by presburger 
 qed
 
 end (* residues_prime_gt2 context *)
 end
diff --git a/thys/Design_Theory/Resolvable_Designs.thy b/thys/Design_Theory/Resolvable_Designs.thy
--- a/thys/Design_Theory/Resolvable_Designs.thy
+++ b/thys/Design_Theory/Resolvable_Designs.thy
@@ -1,223 +1,223 @@
 (* Title: Resolvable_Designs.thy
    Author: Chelsea Edmonds
 *)
 
 section \<open>Resolvable Designs\<close>
 text \<open>Resolvable designs have further structure, and can be "resolved" into a set of resolution 
 classes. A resolution class is a subset of blocks which exactly partitions the point set. 
 Definitions based off the handbook \<^cite>\<open>"colbournHandbookCombinatorialDesigns2007"\<close>
  and Stinson \<^cite>\<open>"stinsonCombinatorialDesignsConstructions2004"\<close>.
 This theory includes a proof of an alternate statement of Bose's theorem\<close>
 
 theory Resolvable_Designs imports BIBD
 begin
 
 subsection \<open>Resolutions and Resolution Classes\<close>
 text \<open>A resolution class is a partition of the point set using a set of blocks from the design 
 A resolution is a group of resolution classes partitioning the block collection\<close>
 
 context incidence_system
 begin 
 
 definition resolution_class :: "'a set set \<Rightarrow> bool" where
 "resolution_class S \<longleftrightarrow> partition_on \<V> S \<and> (\<forall> bl \<in> S . bl \<in># \<B>)"
 
 lemma resolution_classI [intro]: "partition_on \<V>  S \<Longrightarrow> (\<And> bl . bl \<in> S \<Longrightarrow> bl \<in># \<B>) 
     \<Longrightarrow> resolution_class S"
   by (simp add: resolution_class_def)
 
 lemma resolution_classD1: "resolution_class S \<Longrightarrow> partition_on \<V> S"
   by (simp add: resolution_class_def)
 
 lemma resolution_classD2: "resolution_class S \<Longrightarrow>  bl \<in> S \<Longrightarrow> bl \<in># \<B>"
   by (simp add: resolution_class_def)
 
 lemma resolution_class_empty_iff: "resolution_class {} \<longleftrightarrow> \<V>  = {}"
   by (auto simp add: resolution_class_def partition_on_def)
 
 lemma resolution_class_complete: "\<V>  \<noteq> {} \<Longrightarrow> \<V>  \<in># \<B> \<Longrightarrow> resolution_class {\<V>}"
   by (auto simp add: resolution_class_def partition_on_space)
 
 lemma resolution_class_union: "resolution_class S \<Longrightarrow> \<Union>S = \<V> "
   by (simp add: resolution_class_def partition_on_def)
 
 lemma (in finite_incidence_system) resolution_class_finite: "resolution_class S \<Longrightarrow> finite S"
   using finite_elements finite_sets by (auto simp add: resolution_class_def)
 
 lemma (in design) resolution_class_sum_card: "resolution_class S \<Longrightarrow> (\<Sum>bl \<in> S . card bl) = \<v>"
   using resolution_class_union finite_blocks
   by (auto simp add: resolution_class_def partition_on_def card_Union_disjoint)
 
 definition resolution:: "'a set multiset multiset \<Rightarrow> bool" where
 "resolution P \<longleftrightarrow> partition_on_mset \<B> P \<and> (\<forall> S \<in># P . distinct_mset S \<and> resolution_class (set_mset S))"
 
 lemma resolutionI : "partition_on_mset \<B> P \<Longrightarrow> (\<And> S . S \<in>#P \<Longrightarrow> distinct_mset S) \<Longrightarrow> 
     (\<And> S . S\<in># P \<Longrightarrow> resolution_class (set_mset S)) \<Longrightarrow> resolution P"
   by (simp add: resolution_def)
 
 lemma (in proper_design) resolution_blocks: "distinct_mset \<B> \<Longrightarrow> disjoint (set_mset \<B>) \<Longrightarrow> 
     \<Union>(set_mset \<B>) = \<V> \<Longrightarrow> resolution {#\<B>#}"
   unfolding resolution_def resolution_class_def partition_on_mset_def partition_on_def
   using design_blocks_nempty blocks_nempty by auto
 
 end
 
 subsection \<open>Resolvable Design Locale\<close>
 text \<open>A resolvable design is one with a resolution P\<close>
 locale resolvable_design = design + 
   fixes partition :: "'a set multiset multiset" ("\<P>")
   assumes resolvable: "resolution \<P>"
 begin
 
 lemma resolutionD1: "partition_on_mset \<B> \<P>"
   using resolvable by (simp add: resolution_def)
 
 lemma resolutionD2: "S \<in>#\<P> \<Longrightarrow> distinct_mset S" 
   using resolvable by (simp  add: resolution_def)
 
 lemma resolutionD3: " S\<in># \<P> \<Longrightarrow> resolution_class (set_mset S)"
   using resolvable by (simp add: resolution_def)
 
 lemma resolution_class_blocks_disjoint: "S \<in># \<P> \<Longrightarrow> disjoint (set_mset S)"
   using resolutionD3 by (simp add: partition_on_def resolution_class_def) 
 
 lemma resolution_not_empty: "\<B> \<noteq> {#} \<Longrightarrow> \<P> \<noteq> {#}"
   using partition_on_mset_not_empty resolutionD1 by auto 
 
 lemma resolution_blocks_subset: "S \<in># \<P> \<Longrightarrow> S \<subseteq># \<B>"
   using partition_on_mset_subsets resolutionD1 by auto
 
 end
 
 lemma (in incidence_system) resolvable_designI [intro]: "resolution \<P> \<Longrightarrow> design \<V> \<B> \<Longrightarrow> 
     resolvable_design \<V> \<B> \<P>"
   by (simp add: resolvable_design.intro resolvable_design_axioms.intro)
 
 subsection \<open>Resolvable Block Designs\<close>
 text \<open>An RBIBD is a resolvable BIBD - a common subclass of interest for block designs\<close>
 locale r_block_design = resolvable_design + block_design
 begin
 lemma resolution_class_blocks_constant_size: "S \<in># \<P> \<Longrightarrow> bl \<in># S \<Longrightarrow> card bl = \<k>"
   by (metis resolutionD3 resolution_classD2 uniform_alt_def_all)
 
 lemma resolution_class_size1: 
   assumes "S \<in># \<P>"
   shows "\<v> = \<k> * size S"
 proof - 
   have "(\<Sum>bl \<in># S . card bl) = (\<Sum>bl \<in> (set_mset S) . card bl)" using resolutionD2 assms
     by (simp add:  sum_unfold_sum_mset)
   then have eqv: "(\<Sum>bl \<in># S . card bl) = \<v>" using resolutionD3 assms resolution_class_sum_card
     by presburger 
   have "(\<Sum>bl \<in># S . card bl) = (\<Sum>bl \<in># S . \<k>)" using resolution_class_blocks_constant_size assms 
     by auto
   thus ?thesis using eqv by auto
 qed
 
 lemma resolution_class_size2: 
   assumes "S \<in># \<P>"
   shows "size S = \<v> div \<k>"
   using resolution_class_size1 assms
   by (metis nonzero_mult_div_cancel_left not_one_le_zero k_non_zero)
 
 lemma resolvable_necessary_cond_v: "\<k> dvd \<v>"
 proof -
   obtain S where s_in: "S \<in>#\<P>" using resolution_not_empty design_blocks_nempty by blast
   then have "\<k> * size S = \<v>" using resolution_class_size1 by simp 
   thus ?thesis by (metis dvd_triv_left) 
 qed
 
 end
 
 locale rbibd = r_block_design + bibd
  
 begin
 
 lemma resolvable_design_num_res_classes: "size \<P> = \<r>"
 proof - 
   have k_ne0: "\<k> \<noteq> 0" using k_non_zero by auto 
   have f1: "\<b> = (\<Sum>S \<in># \<P> . size S)"
     by (metis partition_on_msetD1 resolutionD1 size_big_union_sum)
   then have "\<b> = (\<Sum>S \<in># \<P> . \<v> div \<k>)" using resolution_class_size2 f1 by auto
   then have f2: "\<b> = (size \<P>) * (\<v> div \<k>)" by simp
   then have "size \<P> = \<b> div (\<v> div \<k>)"
     using b_non_zero by auto 
   then have "size \<P> = (\<b> * \<k>) div \<v>" using f2 resolvable_necessary_cond_v
     by (metis div_div_div_same div_dvd_div dvd_triv_right k_ne0 nonzero_mult_div_cancel_right)
   thus ?thesis using necessary_condition_two
     by (metis nonzero_mult_div_cancel_left not_one_less_zero t_design_min_v) 
 qed
 
 lemma resolvable_necessary_cond_b: "\<r> dvd \<b>"
 proof -
   have f1: "\<b> = (\<Sum>S \<in># \<P> . size S)"
     by (metis partition_on_msetD1 resolutionD1 size_big_union_sum)
   then have "\<b> = (\<Sum>S \<in># \<P> . \<v> div \<k>)" using resolution_class_size2 f1 by auto
   thus ?thesis using resolvable_design_num_res_classes by simp
 qed
 
 subsubsection \<open>Bose's Inequality\<close>
 text \<open>Boses inequality is an important theorem on RBIBD's. This is a proof 
 of an alternate statement of the thm, which does not require a linear algebraic approach, 
 taken directly from Stinson \<^cite>\<open>"stinsonCombinatorialDesignsConstructions2004"\<close>\<close>
 theorem bose_inequality_alternate: "\<b> \<ge> \<v> + \<r> - 1 \<longleftrightarrow> \<r> \<ge> \<k> + \<Lambda>"
 proof - 
   from necessary_condition_two v_non_zero have r: \<open>\<r> = \<b> * \<k> div \<v>\<close>
     by (metis div_mult_self1_is_m)
   define k b v l r where intdefs: "k \<equiv> (int \<k>)" "b \<equiv> int \<b>" "v = int \<v>" "l \<equiv> int \<Lambda>" "r \<equiv> int \<r>"
   have kdvd: "k dvd (v * (r - k))"
     using intdefs
     by (simp add: resolvable_necessary_cond_v)
   have necess1_alt: "l * v - l = r * (k - 1)" using necessary_condition_one intdefs 
     by (smt (verit) diff_diff_cancel int_ops(2) int_ops(6) k_non_zero nat_mult_1_right of_nat_0_less_iff 
         of_nat_mult right_diff_distrib' v_non_zero)
   then have v_eq: "v = (r * (k - 1) + l) div l" 
     using necessary_condition_one index_not_zero intdefs
     by (metis diff_add_cancel nonzero_mult_div_cancel_left not_one_le_zero of_nat_mult 
-        unique_euclidean_semiring_with_nat_class.of_nat_div) 
+        linordered_euclidean_semiring_class.of_nat_div) 
   have ldvd: " \<And> x. l dvd (x * (r * (k - 1) + l))" 
     by (metis necess1_alt diff_add_cancel dvd_mult dvd_triv_left) 
   have "(b \<ge> v + r - 1) \<longleftrightarrow> ((\<v> * r) div k \<ge> v + r - 1)"
     using necessary_condition_two k_non_zero intdefs
     by (metis (no_types, lifting) nonzero_mult_div_cancel_right not_one_le_zero of_nat_eq_0_iff of_nat_mult)
   also have  "... \<longleftrightarrow> (((v * r) - (v * k)) div k \<ge> r - 1)"
     using k_non_zero k_non_zero r intdefs
     by (simp add: of_nat_div algebra_simps)
       (smt (verit, ccfv_threshold) One_nat_def div_mult_self4 of_nat_1 of_nat_mono)
   also have f2: " ... \<longleftrightarrow> ((v * ( r - k)) div k \<ge> ( r - 1))"
     using int_distrib(3) by (simp add: mult.commute)
   also have f2: " ... \<longleftrightarrow> ((v * ( r - k)) \<ge> k * ( r - 1))" 
     using k_non_zero kdvd intdefs by auto
   also have "... \<longleftrightarrow> ((((r * (k - 1) + l ) div l) * (r - k)) \<ge> k * (r - 1))"
     using v_eq by presburger 
   also have "... \<longleftrightarrow> ( (r - k) * ((r * (k - 1) + l ) div l) \<ge> (k * (r - 1)))" 
     by (simp add: mult.commute)
   also have " ... \<longleftrightarrow> ( ((r - k) * (r * (k - 1) + l )) div l \<ge> (k * (r - 1)))"
     using div_mult_swap necessary_condition_one intdefs
     by (metis diff_add_cancel dvd_triv_left necess1_alt) 
   also have " ... \<longleftrightarrow> (((r - k) * (r * (k - 1) + l ))  \<ge>  l * (k * (r - 1)))" 
     using ldvd[of "(r - k)"] dvd_mult_div_cancel index_not_zero mult_strict_left_mono intdefs
     by (smt (verit) b_non_zero bibd_block_number bot_nat_0.extremum_strict div_0 less_eq_nat.simps(1) 
       mult_eq_0_iff mult_left_le_imp_le mult_left_mono of_nat_0 of_nat_le_0_iff of_nat_le_iff of_nat_less_iff)
   also have 1: "... \<longleftrightarrow> (((r - k) * (r * (k - 1))) + ((r - k) * l )  \<ge>  l * (k * (r - 1)))" 
     by (simp add: distrib_left) 
   also have "... \<longleftrightarrow> (((r - k) * r * (k - 1)) \<ge> l * k * (r - 1) - ((r - k) * l ))" 
     using mult.assoc by linarith 
   also have "... \<longleftrightarrow> (((r - k) * r * (k - 1)) \<ge> (l * k * r) - (l * k) - ((r * l) -(k * l )))" 
     using distrib_right by (simp add: distrib_left right_diff_distrib' left_diff_distrib') 
   also have "... \<longleftrightarrow> (((r - k) * r * (k - 1)) \<ge> (l * k * r)  - ( l * r))" 
     by (simp add: mult.commute) 
   also have "... \<longleftrightarrow> (((r - k) * r * (k - 1)) \<ge> (l  * (k * r))  - ( l * r))" 
     by linarith  
   also have "... \<longleftrightarrow> (((r - k) * r * (k - 1)) \<ge> (l  * (r * k))  - ( l * r))" 
     by (simp add: mult.commute)
   also have "... \<longleftrightarrow> (((r - k) * r * (k - 1)) \<ge> l * r * (k - 1))"
     by (simp add:  mult.assoc int_distrib(4)) 
   finally have "(b \<ge> v + r - 1) \<longleftrightarrow> (r \<ge> k + l)"
     using index_lt_replication mult_right_le_imp_le r_gzero mult_cancel_right k_non_zero intdefs
     by (smt (z3) of_nat_0_less_iff of_nat_1 of_nat_le_iff of_nat_less_iff)
   then have "\<b> \<ge> \<v> + \<r> - 1 \<longleftrightarrow> \<r> \<ge> \<k> + \<Lambda>"
     using k_non_zero le_add_diff_inverse of_nat_1 of_nat_le_iff intdefs by linarith 
   thus ?thesis by simp
 qed
 end
 end
\ No newline at end of file
diff --git a/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Lemmas.thy b/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Lemmas.thy
--- a/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Lemmas.thy
+++ b/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Lemmas.thy
@@ -1,724 +1,724 @@
 section \<open> Technical Lemmas \<close>
 text \<open>We show three lemmas used in the proof of both main theorems.\<close>
 
 theory Polygonal_Number_Theorem_Lemmas
   imports "Three_Squares.Three_Squares"
 
 begin
 
 subsection \<open> Lemma 1.10 in \cite{nathanson1996} \<close>
 text \<open>This lemma is split into two parts. We modify the proof given in \cite{nathanson1996} slightly as we require the second result to hold for $l=2$ in the proof of Legendre's polygonal number theorem.\<close>
 
 theorem interval_length_greater_than_four:
   fixes m N L :: real
   assumes "m \<ge> 3"
   assumes "N \<ge> 2*m"
   assumes "L = (2/3 + sqrt (8*N/m - 8)) - (1/2 + sqrt (6*N/m - 3))"
   shows "N \<ge> 108*m \<Longrightarrow> L > 4" 
 
 proof -
   assume asm: "N \<ge> 108*m"
   show "L > 4"
     proof -
       define x :: real where "x = N / m"
       define l :: real where "l = 4"
       define l_0 :: real where "l_0 = 4 - 1/6"
       have 0: "x \<ge> 2" unfolding x_def using assms(2)
         by (metis assms(1) divide_right_mono dual_order.trans linorder_le_cases mult.commute mult_1 nonzero_mult_div_cancel_left numeral_le_one_iff semiring_norm(70) zero_le_square)
       have 1: "L = sqrt (8*x - 8) - sqrt (6*x - 3) + 1/6" by (auto simp add: x_def assms(3))
       hence 2: "L > l \<longleftrightarrow> sqrt (8*x - 8) > sqrt (6*x - 3) + l_0" unfolding l_0_def l_def by auto
       have 3: "sqrt (8*x - 8) > sqrt (6*x - 3) + l_0 \<longleftrightarrow> 2*x - l_0^2 - 5 > 2*l_0 * sqrt (6*x - 3)"
       proof
         assume "sqrt (8*x - 8) > sqrt (6*x - 3) + l_0"
         hence "(sqrt (8*x - 8))^2 > (sqrt (6*x - 3) + l_0)^2" 
           using l_0_def asm by (smt (verit, ccfv_SIG) "0" divide_less_eq_1_pos one_power2 pos2 power_mono_iff real_less_rsqrt)
         hence "8*x - 8 > 6*x - 3 + l_0^2 + 2*l_0* sqrt (6*x - 3)"
           by (smt (verit, del_insts) "0" power2_sum real_sqrt_pow2_iff)
         thus "2*x - l_0^2 - 5 > 2*l_0* sqrt (6*x - 3)" by auto
       next
         assume "2*x - l_0^2 - 5 > 2*l_0* sqrt (6*x - 3)"
         hence "8*x - 8 > 6*x - 3 + l_0^2 + 2*l_0* sqrt (6*x - 3)" by auto
         hence "(sqrt (8*x - 8))^2 > (sqrt (6*x - 3) + l_0)^2"
           by (smt (verit, best) 0 power2_sum real_sqrt_pow2_iff)
         thus "sqrt (8*x - 8) > sqrt (6*x - 3) + l_0"
           using 0 real_less_rsqrt by force 
       qed
       have "2*x - l_0^2 - 5 > 2*l_0* sqrt (6*x - 3) \<longleftrightarrow> 4*x*(x - (7*l_0^2 + 5)) + (l_0^2 + 5)^2 + 12*l_0^2 > 0"
       proof
         assume "2*x - l_0^2 - 5 > 2*l_0* sqrt (6*x - 3)"
         hence "(2*x - l_0^2 - 5)^2 > (2*l_0* sqrt (6*x - 3))^2"
           by (smt (verit, del_insts) "0" asm l_0_def le_divide_eq_1_pos less_1_mult one_power2 pos2 power_mono_iff sqrt_le_D)
         thus "4*x*(x - (7*l_0^2 + 5)) + (l_0^2 + 5)^2 + 12*l_0^2 > 0"
           using 0 by (simp add: algebra_simps power2_eq_square power4_eq_xxxx)
       next
         assume "4*x*(x - (7*l_0^2 + 5)) + (l_0^2 + 5)^2 + 12*l_0^2 > 0"
         hence "(2*x - l_0^2 - 5)^2 > (2*l_0* sqrt (6*x - 3))^2"
           using 0 by (simp add: algebra_simps power2_eq_square power4_eq_xxxx)
         from assms(1) have "m > 0" by auto
         hence "2*x \<ge> 2*108"
           using x_def asm by (simp add: le_divide_eq)
         hence "2*x - l_0^2 - 5 \<ge> 2*108 - (4-1/6)*(4-1/6) - 5" unfolding l_0_def by (auto simp add: power2_eq_square)
         hence "2*x - l_0^2 - 5 > 0" by auto
         thus "2*x - l_0^2 - 5 > 2*l_0* sqrt (6*x - 3)"
           using \<open>(2*x - l_0^2 - 5)^2 > (2*l_0* sqrt (6*x - 3))^2\<close> using power2_less_imp_less by fastforce
       qed
       from assms(1) have "m > 0" by auto
       hence "x \<ge> 108" using x_def asm by (simp add: le_divide_eq)
       have "7*(4-1/6)*(4-1/6) + 5 < (108::real)" by simp
       hence "7*l_0^2 + 5 < 108" unfolding l_0_def by (auto simp add: power2_eq_square)
       hence "x \<ge> 7*l_0^2 + 5" using \<open>108 \<le> x\<close> by auto
       hence "4*x*(x - (7*l_0^2 + 5)) + (l_0^2 + 5)^2 + 12*l_0^2 > 0"
         by (smt (verit) mult_nonneg_nonneg power2_less_eq_zero_iff zero_le_power2)
       thus ?thesis
         using "2" "3" \<open>(2 * l_0 * sqrt (6 * x - 3) < 2 * x - l_0\<^sup>2 - 5) = (0 < 4 * x * (x - (7 * l_0\<^sup>2 + 5)) + (l_0\<^sup>2 + 5)\<^sup>2 + 12 * l_0\<^sup>2)\<close> l_def by blast
     qed
   qed
 
 theorem interval_length_greater_than_lm:
   fixes m N :: real
   fixes L l :: real
   assumes "m \<ge> 3"
   assumes "N \<ge> 2*m"
   assumes "L = (2/3 + sqrt (8*N/m - 8)) - (1/2 + sqrt (6*N/m - 3))"
   shows "l \<ge> 2 \<and> N \<ge> 7*l^2*m^3 \<Longrightarrow> L > l*m"
 
 proof -
   assume asm: "l \<ge> 2 \<and> N \<ge> 7*l^2*m^3"
   show "L > l*m"
   proof -
     from asm have asm1: "l \<ge> 2" and asm2: "N \<ge> 7*l^2*m^3" by auto
     define x :: real where "x = N / m"
     define l_0 :: real where "l_0 = l*m - 1/6" 
     have "l_0 > 0" using l_0_def asm1 assms(1)
       by (smt (verit, ccfv_threshold) le_divide_eq_1 mult_le_cancel_left2 of_int_le_1_iff)
     have 0: "x \<ge> 2" using x_def assms(1,2) by (simp add: pos_le_divide_eq)
     have 1: "L = sqrt (8*x - 8) - sqrt (6*x - 3) + 1/6" by (auto simp add: x_def assms(3))
     hence 2: "L > l*m \<longleftrightarrow> sqrt (8*x - 8) > sqrt (6*x - 3) + l_0" by (auto simp add: l_0_def)
     have 3: "sqrt (8*x - 8) > sqrt (6*x - 3) + l_0 \<longleftrightarrow> 2*x - l_0^2 - 5 > 2*l_0 * sqrt (6*x - 3)"
     proof
       assume "sqrt (8*x - 8) > sqrt (6*x - 3) + l_0"
       hence "(sqrt (8*x - 8))^2 > (sqrt (6*x - 3) + l_0)^2" 
         using l_0_def asm1 by (smt (verit, best) \<open>0 < l_0\<close> real_le_lsqrt real_sqrt_four real_sqrt_less_iff real_sqrt_pow2_iff)
       hence "8*x - 8 > 6*x - 3 + l_0^2 + 2* l_0 * sqrt (6*x - 3)"
         by (smt (verit, del_insts) "0" power2_sum real_sqrt_pow2_iff)
       thus "2*x - l_0^2 - 5 > 2*l_0 * sqrt (6*x - 3)" by auto
     next
       assume "2*x - l_0^2 - 5 > 2*l_0 * sqrt (6*x - 3)"
       hence "8*x - 8 > 6*x - 3 + l_0^2 + 2*l_0 * sqrt (6*x - 3)" by auto
       hence "(sqrt (8*x - 8))^2 > (sqrt (6*x - 3) + l_0)^2"
         by (smt (verit, del_insts) "0" power2_sum real_sqrt_pow2_iff)
       thus "sqrt (8*x - 8) > sqrt (6*x - 3) + l_0"
         using 0 real_less_rsqrt by force 
     qed
     have "2*x - l_0^2 - 5 > 2*l_0 * sqrt (6*x - 3) \<longleftrightarrow> 4*x*(x - (7*l_0^2 + 5)) + (l_0^2 + 5)^2 + 12*l_0^2 > 0"
     proof
       assume "2*x - l_0^2 - 5 > 2*l_0 * sqrt (6*x - 3)"
       have "(2*x - l_0^2 - 5)^2 > (2*l_0 * sqrt (6*x - 3))^2"
         using \<open>0 < l_0\<close> by (smt (verit, ccfv_SIG) 0 \<open>2 * l_0 * sqrt (6 * x - 3) < 2 * x - l_0\<^sup>2 - 5\<close> pos2 power_strict_mono real_sqrt_ge_zero zero_le_mult_iff)
       thus "4*x*(x - (7*l_0^2 + 5)) + (l_0^2 + 5)^2 + 12*l_0^2 > 0"
         using 0 by (simp add: algebra_simps power2_eq_square power4_eq_xxxx)
     next
       assume "4*x*(x - (7*l_0^2 + 5)) + (l_0^2 + 5)^2 + 12*l_0^2 > 0"
       hence "(2*x - l_0^2 - 5)^2 > (2*l_0 * sqrt (6*x - 3))^2"
         using 0 by (simp add: algebra_simps power2_eq_square power4_eq_xxxx)
       have "m > 0" using assms(1) by simp
       hence "x \<ge> 7*l^2*m^2" 
         unfolding x_def using asm2 assms(1)
         by (simp add: mult_imp_le_div_pos power2_eq_square power3_eq_cube)
       hence 4: "2*x - l_0^2 - 5 \<ge> 14*l^2*m^2 - (l*m-1/6)^2 - 5" 
         by (simp add: x_def l_0_def power2_eq_square)
       have "(l*m-(1/6::real))^2 = (l*m)^2 - l*m/3 + (1/36::real)"
         apply (simp add: power2_eq_square)
         by argo
       hence "14*l^2*m^2 - (l*m-1/6)^2 - 5 = 14*l^2*m^2 - l^2*m^2 + l*m/3 - 1/36 - 5"
         using 4 by (auto simp add: power2_eq_square)
       hence "14*l^2*m^2 - l^2*m^2 + l*m/3 - 1/36 - 5 = 13*l^2*m^2  + l*m/3 - 1/36 - 5" by argo
       from asm1 assms(1) have 5: "l*m/3 > 0" by simp
       have "l > 0" using asm1 by auto 
       hence "l*l \<ge> 2*2" using asm1 mult_mono' zero_le_numeral by blast
       have "m > 0" using assms(1) by auto
       hence "m*m \<ge> 3*3"
         by (metis assms(1) less_eq_real_def mult_le_less_imp_less zero_less_numeral)
       hence "13*m*m - 1 \<ge> 13*3*3-1" by simp
       have "3*3 > (0::real)" by auto
       hence "13*l*l*m*m \<ge>(13::real)*2*2*3*3" using \<open>l*l \<ge> 2*2\<close> asm1
         by (meson \<open>0 < l\<close> \<open>0 < m\<close> assms(1) less_eq_real_def mult_mono split_mult_pos_le zero_le_numeral)
       hence "13*l^2*m^2  + l*m/3 - 1/36 - 5 \<ge> 13*2*2*3*3-1/36-(5::real)"
         using 5 by (auto simp add: power2_eq_square)
       have "13*3*3*3*3-1/36-(5::real) > 0" by auto
       hence "2*x - l_0^2 - 5 > 0"
         using "4" \<open>13 * 2 * 2 * 3 * 3 - 1 / 36 - 5 \<le> 13 * l\<^sup>2 * m\<^sup>2 + l * m / 3 - 1 / 36 - 5\<close> \<open>14 * l\<^sup>2 * m\<^sup>2 - (l * m - 1 / 6)\<^sup>2 - 5 = 14 * l\<^sup>2 * m\<^sup>2 - l\<^sup>2 * m\<^sup>2 + l * m / 3 - 1 / 36 - 5\<close> by force
       thus "2*x - l_0^2 - 5 > 2*l_0 * sqrt (6*x - 3)"
         by (smt (verit) \<open>(2 * l_0 * sqrt (6 * x - 3))\<^sup>2 < (2 * x - l_0\<^sup>2 - 5)\<^sup>2\<close> power_mono)
     qed
     have "(1/6)^2 * (36::real) = 1" by (auto simp add: power2_eq_square)
     from assms(1) have "m > 0" by auto
     hence "x \<ge> 7*l^2*m^2" unfolding x_def using asm2
       by (simp add: pos_le_divide_eq power2_eq_square power3_eq_cube)
     from asm1 have "l > 0" by auto
     from assms(1) asm1 \<open>m > 0\<close> \<open>l > 0\<close> have "l*m \<ge> 2*(3::real)"
       by (metis mult_less_cancel_right mult_mono verit_comp_simplify1(1) verit_comp_simplify1(3) zero_le_numeral)
     hence "-2*7*l*m/6 + 7*(1/6)*(1/6) + 5 < (0::real)" by simp
     hence "7*l^2*m^2 > 7*l_0^2 + (5::real)" unfolding l_0_def
       apply (auto simp add: power2_eq_square)
       by argo
     hence "x \<ge> 7*l_0^2 + 5"
       using \<open>7 * l\<^sup>2 * m\<^sup>2 \<le> x\<close> by linarith
     hence "4*x*(x - (7*l_0^2 + 5)) + (l_0^2 + 5)^2 + 12*l_0^2 > 0"
       by (smt (verit) mult_nonneg_nonneg power2_less_eq_zero_iff zero_le_power2)
     thus ?thesis
       using "2" "3" \<open>(2 * l_0 * sqrt (6 * x - 3) < 2 * x - l_0\<^sup>2 - 5) = (0 < 4 * x * (x - (7 * l_0\<^sup>2 + 5)) + (l_0\<^sup>2 + 5)\<^sup>2 + 12 * l_0\<^sup>2)\<close> by fastforce
   qed
 qed
 
 lemmas interval_length_greater_than_2m [simp] = interval_length_greater_than_lm [where l=2, simplified]
 
 subsection \<open> Lemma 1.11 in \cite{nathanson1996} \<close>
 
 text \<open> We show Lemma 1.11 in \cite{nathanson1996} which is also known as Cauchy's Lemma.\<close>
 
 theorem Cauchy_lemma:
   fixes m N a b r :: real
   assumes "m \<ge> 3" "N \<ge> 2*m"
   and "0 \<le> a" "0 \<le> b" "0 \<le> r" "r < m"
   and "N = m*(a - b)/2 + b + r"
   and "1/2 + sqrt (6*N/m - 3) \<le> b \<and> b \<le> 2/3 + sqrt (8*N/m - 8)"
   shows "b^2 < 4*a \<and> 3*a < b^2 + 2*b + 4"
 
 proof-
   from assms have asm1: "1/2 + sqrt (6*N/m - 3) \<le> b" and asm2: "b \<le> 2/3 + sqrt (8*N/m - 8)" by auto
   have "N - b - r = m*(a - b)/2" using assms(7) by simp
   hence "a = (N - b - r)*2/m + b" using assms(1) by simp
   hence "a = b - 2/m * b + 2 * (N - r)/m"
     apply (simp add: algebra_simps)
     by (smt (verit, del_insts) add_divide_distrib)
   hence a: "a = b*(1 - 2/m) + 2*(N - r)/m"
     by (simp add: right_diff_distrib')
   have "b^2 < 4*a"
   proof -
     from a have 0: "b^2 - 4*a = b^2 - 4*(1 - 2/m)*b - 8*(N-r)/m" by simp
     have "3/m \<le> 1" using assms(1) by simp
     hence 1: "2/3 \<le> 2*(1 - 2/m)" by simp
     have "N/m - 1 < N/m - r/m" using assms(1,6) by simp
     hence "sqrt(8*(N/m - 1)) < sqrt (8*((N - r)/m))" by (simp add: diff_divide_distrib)
     hence 2: "sqrt(8*N/m - 8) < sqrt (8*((N - r)/m))" by simp
     have "2/3 + sqrt (8*N/m - 8) < 2*(1 - 2/m) + sqrt (8*((N-r)/m))"
       using 1 2 by linarith
     hence "b < 2*(1-2/m) + sqrt (8*(N - r)/m)" using asm2 by simp
     hence 3: "b < 2*(1-2/m) + sqrt (4*(1-2/m)^2 + 8*(N - r)/m)"
       by (smt (verit, best) power2_less_0 real_sqrt_le_iff)
     define r1 where "r1 = 2*(1-2/m) - sqrt (4*(1-2/m)^2 + 8*(N - r)/m)"
     define r2 where "r2 = 2*(1-2/m) + sqrt (4*(1-2/m)^2 + 8*(N - r)/m)"
 
     have "r1*r2 = (2*(1-2/m) - sqrt (4*(1-2/m)^2 + 8*(N - r)/m))*(2*(1-2/m) + sqrt (4*(1-2/m)^2 + 8*(N - r)/m))"
       using r1_def r2_def by simp
     hence "r1*r2 = 2*(1-2/m)*(2*(1-2/m) + sqrt (4*(1-2/m)^2 + 8*(N - r)/m)) - 
 sqrt (4*(1-2/m)^2 + 8*(N - r)/m)*(2*(1-2/m) + sqrt (4*(1-2/m)^2 + 8*(N - r)/m))" 
       by (simp add: Rings.ring_distribs(3)) 
     hence "r1*r2 = (2*(1-2/m))^2+2*(1-2/m)* sqrt (4*(1-2/m)^2 + 8*(N - r)/m) - 2*(1-2/m)* sqrt (4*(1-2/m)^2 + 8*(N - r)/m)
 - (sqrt (4*(1-2/m)^2 + 8*(N - r)/m))^2" by (simp add: distrib_left power2_eq_square)
     hence "r1*r2 = (2*(1-2/m))^2 -(sqrt (4*(1-2/m)^2 + 8*(N - r)/m))^2" by simp
 
     hence "r1 * r2  = 4*(1-2/m)^2 - 4*(1-2/m)^2 - 8*(N - r)/m"
       using assms(1) assms(2) assms(6) four_x_squared
       by (smt (verit) divide_nonneg_nonneg real_sqrt_pow2_iff zero_compare_simps(12))
     hence r1_times_r2:"r1*r2 = -8*(N-r)/m" by linarith
 
     have "(b-r1)*(b-r2) = b*(b-r2) - r1*(b-r2)" using cross3_simps(28) by blast
     hence "(b-r1)*(b-r2) = b^2-b*r2-b*r1+r1*r2" by (simp add: power2_eq_square right_diff_distrib)
     hence "(b-r1)*(b-r2) = b^2-b*(2*(1-2/m) + sqrt (4*(1-2/m)^2 + 8*(N - r)/m))-b*(2*(1-2/m) - sqrt (4*(1-2/m)^2 + 8*(N - r)/m))+r1*r2"
       using r1_def r2_def by simp
     hence "(b-r1)*(b-r2) = b^2-b*2*(1-2/m)-b* sqrt (4*(1-2/m)^2 + 8*(N - r)/m)-b*(2*(1-2/m) - sqrt (4*(1-2/m)^2 + 8*(N - r)/m)) +r1*r2" 
       by (simp add: distrib_left)
     hence "(b-r1)*(b-r2) = b^2-b*2*(1-2/m)-b* sqrt (4*(1-2/m)^2 + 8*(N - r)/m)-b*2*(1-2/m)+b* sqrt (4*(1-2/m)^2 + 8*(N - r)/m)+r1*r2"
       by (simp add: Rings.ring_distribs(4))
     hence "(b-r1)*(b-r2) = b^2-b*4*(1-2/m)+r1*r2" by simp
     hence "(b-r1)*(b-r2) = b^2 - 4*(1 - 2/m)*b - 8*(N-r)/m" using r1_times_r2
       by (simp add: \<open>r1 * r2 = 4 * (1 - 2 / m)\<^sup>2 - 4 * (1 - 2 / m)\<^sup>2 - 8 * (N - r) / m\<close>)
     hence "b^2 - 4*(1 - 2/m)*b - 8*(N-r)/m < 0" using 3 assms(4)
       by (smt (verit, del_insts) \<open>r1 * r2 = 4 * (1 - 2 / m)\<^sup>2 - 4 * (1 - 2 / m)\<^sup>2 - 8 * (N - r) / m\<close> assms(1) assms(2) assms(6) divide_pos_pos mult_nonneg_nonneg mult_pos_neg r2_def)
     thus ?thesis using 0 by simp
   qed
   have "3*a < b^2 + 2*b + 4"
   proof - 
     from a have 4: "b^2 + 2*b + 4 - 3*a = b^2 - (1-6/m)*b - (6*(N-r)/m - 4)" by argo
     have 5: "1/2 > 1/2 - 3/m" using assms(1) by simp
     hence "1/2 - 3/m < 1" by linarith
     also have "1/2 - 3/m > -1" using assms(1)
       by (smt (verit) divide_le_0_1_iff less_divide_eq_1_pos)
     hence "(1/2 - 3/m)^2 < 1" 
       by (metis (no_types, opaque_lifting) calculation less_eq_real_def power2_eq_1_iff square_le_1 verit_comp_simplify1(3))
     hence 6: "sqrt (6*N/m - 3) > sqrt ((1/2 - 3/m)^2 + 6*N/m - 4)" using assms(1) by simp
     from asm1 5 6 have "b > (1/2 - 3/m) + sqrt ((1/2 - 3/m)^2 + 6*N/m - 4)" by linarith
     hence 7: "b > (1/2 - 3/m) + sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4)"
       by (smt (verit, ccfv_SIG) assms(1) assms(5) divide_right_mono real_sqrt_le_mono)
     define s1 where "s1 = (1/2 - 3/m) - sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4)"
     define s2 where "s2 = (1/2 - 3/m) + sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4)"
     have "s1* s2=(1/2-3/m)*((1/2 - 3/m) + sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4))- 
 sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4)*((1/2 - 3/m) + sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4))"
       using s1_def s2_def Rings.ring_distribs(3) by blast
     hence "s1* s2= (1/2-3/m)^2+(1/2-3/m)* sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4)- 
 sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4)*((1/2 - 3/m) + sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4))"
       by (simp add: nat_distrib(2) power2_eq_square)
     hence "s1* s2= (1/2-3/m)^2+(1/2-3/m)* sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4)-
 (1/2-3/m)* sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4) - (sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4))^2"
       by (smt (verit, ccfv_SIG) Groups.mult_ac(2) Rings.ring_distribs(3) power2_eq_square)
     hence 8:"s1* s2=(1/2-3/m)^2- (sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4))^2" by simp
     from assms(1,6) have "-r/m > -1" by simp
     hence "-6*r/m > -6" by simp
     hence "12 - 4 - 6*r/m > 0" by simp
     hence "12*m/m - 6*r/m - 4 > 0" using assms(1) by simp
     hence "6*(2*m - r)/m - 4 > 0" by argo
     hence "6*(N - r)/m - 4 > 0" using assms(1,2)
       by (smt (verit, best) divide_right_mono)
     hence "s1 * s2 = (1/2 - 3/m)^2 - (1/2 - 3/m)^2 - 6*(N - r)/m + 4" using 8
       by (smt (verit) real_sqrt_pow2_iff zero_le_power2)
 
     have "(b-s1)*(b-s2) = b*(b-s2) - s1*(b-s2)" using cross3_simps(28) by blast
     hence "(b-s1)*(b-s2) = b^2-b* s2-b* s1+s1* s2" by (simp add: power2_eq_square right_diff_distrib)
     hence "(b-s1)*(b-s2) = b^2-b*((1/2 - 3/m) + sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4))-b*((1/2 - 3/m) - sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4))
 + s1* s2" using s1_def s2_def by simp
     hence "(b-s1)*(b-s2) = b^2-b*(1/2 - 3/m)-b* sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4)-b*((1/2 - 3/m) - sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4))
 + s1* s2" by (simp add: nat_distrib(2))
     hence "(b-s1)*(b-s2) = b^2-b*(1/2 - 3/m)-b* sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m - 4)-b*(1/2 - 3/m)+b* sqrt ((1/2 - 3/m)^2 + 6*(N - r)/m-4)+s1* s2"
       by (smt (verit, ccfv_SIG) nat_distrib(2))
     hence "(b-s1)*(b-s2) = b^2-2*b*(1/2 - 3/m)+s1* s2" by simp
     hence "(b-s1)*(b-s2) = b^2-2*b*(1/2 - 3/m)+ (1/2 - 3/m)^2 - (1/2 - 3/m)^2 - 6*(N - r)/m + 4"
       using \<open>s1 * s2 = (1 / 2 - 3 / m)\<^sup>2 - (1 / 2 - 3 / m)\<^sup>2 - 6 * (N - r) / m + 4\<close> by fastforce
     hence "(b-s1)*(b-s2) = b^2-2*b*(1/2-3/m)- 6*(N - r)/m + 4" by simp
     hence "(b-s1)*(b-s2) = b^2-b*(1-6/m)- 6*(N - r)/m + 4" by simp
     hence "(b-s1)*(b-s2) = b^2-b*(1-6/m)- (6*(N - r)/m - 4)" by simp
     hence "b^2 - (1-6/m)*b - (6*(N-r)/m - 4) > 0" using 7 by (smt (verit, del_insts) "8" Groups.mult_ac(2) 
 \<open>s1 * s2 = (1 / 2 - 3 / m)\<^sup>2 - (1 / 2 - 3 / m)\<^sup>2 - 6 * (N - r) / m + 4\<close> real_sqrt_ge_0_iff s1_def s2_def zero_compare_simps(8) zero_le_power2)
     thus ?thesis using 4 by simp
   qed
   show ?thesis by (simp add: \<open>3 * a < b\<^sup>2 + 2 * b + 4\<close> \<open>b\<^sup>2 < 4 * a\<close>)
 qed
 
 lemmas Cauchy_lemma_r_eq_zero = Cauchy_lemma [where r=0, simplified]
 
 subsection \<open> Lemma 1.12 in \cite{nathanson1996} \<close>
 
 lemma not_one:
   fixes a b :: nat
   assumes "a\<ge>1"
   assumes "b\<ge>1"
   assumes "\<exists>k1 :: nat. a = 2*k1+1"
   assumes "\<exists>k2 :: nat. b = 2*k2+1"
   assumes "b^2 < 4*a"
   shows "4*a-b^2 \<noteq> 1"
 
 proof 
   assume "4*a-b^2 = 1"
   hence "b^2 = 4*a-1" by auto
   hence "b^2 mod 4 = (4*a-1) mod 4" by auto
   have "(4*a-1) mod 4 = 3 mod 4" using assms(1) by (simp add: mod_diff_eq_nat)
   hence "b^2 mod 4 = 3" using \<open>b^2 = 4*a-1\<close> mod_less by presburger
   thus "False" using assms by (metis One_nat_def eq_numeral_Suc insert_iff nat.simps(3)
  power_two_mod_four pred_numeral_simps(3) singletonD)
 qed
 
 
 lemma not_two:
   fixes a b :: nat
   assumes "a\<ge>1"
   assumes "b\<ge>1"
   assumes "\<exists>k1 :: nat. a = 2*k1+1"
   assumes 1:"\<exists>k2 :: nat. b = 2*k2+1"
   assumes "b^2 < 4*a"
   shows "4*a-b^2 \<noteq> 2"
 
 proof
   assume "4*a-b^2=2"
   hence "b^2=4*a-2" by auto
   from 1 have 2: "\<not> 2 dvd b^2" by auto
   have "2 dvd (4*a-2)" by auto
   thus "False" using \<open>b^2=4*a-2\<close> 2 by auto
 qed
 
 text \<open>The following lemma shows that given odd positive integers $x,y,z$ and $b$, where $x \geq y \geq z$, we may pick 
 a suitable integer $u$ where $u = z$ or $u = -z$, such that $b+x+y+u \equiv 0 \pmod{4}$.\<close>
 
 lemma suit_z:
   fixes b x y z :: nat
   assumes "odd b \<and> odd x \<and> odd y \<and> odd z"
   assumes "x\<ge>y \<and> y\<ge>z"
   shows "\<exists> u :: int. (u=z \<or> u=-z) \<and> (b+x+y+u) mod 4 = 0" 
 
 proof -
   from assms have 0: "(b+x+y) mod 4 = 1 \<or> (b+x+y) mod 4 = 3" by (metis dvd_refl even_add 
 even_even_mod_4_iff landau_product_preprocess(53) mod_exhaust_less_4)
   from assms have 1: "z mod 4 = 1 \<or> z mod 4 = 3" by (metis dvd_0_right dvd_refl
  even_even_mod_4_iff mod_exhaust_less_4)
 
   have c1:"\<exists>u1::int. (u1=z \<or> u1=-z) \<and> (b+x+y+u1) mod 4 = 0" 
     if asm1:"(b+x+y) mod 4 = 1 \<and> z mod 4 = 3"
   proof -
     from asm1 have 2:"(b+x+y+z) mod 4 = 0" by (metis add_num_simps(1) add_num_simps(7)
  mod_add_eq mod_self numeral_plus_one one_plus_numeral_commute)
     define u1 :: int where "u1=z"
     show "\<exists>u1::int. (u1=z \<or> u1=-z) \<and> (b+x+y+u1) mod 4 = 0" using "2" u1_def
       by (metis Num.of_nat_simps(4) of_nat_0 of_nat_numeral zmod_int)
   qed
 
   have c2:"\<exists>u2::int.(u2=z \<or> u2=-z) \<and> (b+x+y+u2) mod 4 = 0" 
     if asm2:"(b+x+y) mod 4 = 1 \<and> z mod 4 = 1"
   proof -
     from asm2 have 3:"(b+x+y-z) mod 4 = 0" 
       by (metis assms(2) mod_eq_0_iff_dvd mod_eq_dvd_iff_nat trans_le_add2)
     define u2::int where "u2=-z"
     show "\<exists>u2::int.(u2=z \<or> u2=-z) \<and> (b+x+y+u2) mod 4 = 0" using "3" u2_def 
       by (metis Num.of_nat_simps(2) asm2 mod_0
  mod_add_cong more_arith_simps(4) of_nat_numeral zmod_int)
   qed
 
   have c3:"\<exists>u3::int.(u3=z \<or> u3=-z) \<and> (b+x+y+u3) mod 4 = 0" 
     if asm3:"(b+x+y) mod 4 = 3 \<and> z mod 4 = 1"
   proof -
     from asm3 have 4: "(b+x+y+z) mod 4 = 0" by (metis add_num_simps(1) add_num_simps(7)
  mod_add_eq mod_self numeral_plus_one)
     define u3::int where "u3=z"
     show "\<exists>u3::int.(u3=z \<or> u3=-z) \<and> (b+x+y+u3) mod 4 = 0" using "4" u3_def
       by (metis Num.of_nat_simps(4) of_nat_0 of_nat_numeral zmod_int)
   qed
 
   have c4:"\<exists>u4::int.(u4=z \<or> u4=-z) \<and> (b+x+y+u4) mod 4 = 0" 
     if asm4:"(b+x+y) mod 4 = 3 \<and> z mod 4 = 3"
   proof -
     from asm4 have 5: "(b+x+y-z) mod 4 = 0" 
       by (metis assms(2) mod_eq_0_iff_dvd mod_eq_dvd_iff_nat trans_le_add2)
     define u4::int where "u4=-z"
     show "\<exists>u4::int.(u4=z \<or> u4=-z) \<and> (b+x+y+u4) mod 4 = 0" using "5" u4_def by (metis asm4 mod_0
  mod_add_cong more_arith_simps(4) of_nat_numeral zmod_int)
   qed
 
   show ?thesis using assms 0 1 c1 c2 c3 c4 by auto
 qed
 
 lemma four_terms_bin_exp_allsum:
   fixes b s t u v :: int
   assumes "b = s+t+u+v"
   shows "b^2 =  t^2+u^2+s^2+v^2+2*t*u+2 * s * v + 2*t * s + 2*t * v +2*u * s +2*u * v"
 
 proof -
   from assms have "b^2 = (t+u)^2+(s+v)^2+2*(t+u)*(s+v)" by (smt (verit, best) power2_sum)  
   hence b_simp1:"b^2 = (t^2+u^2+2*t*u) + (s^2+v^2+2 * s * v)+2*(t+u)*(s+v)" 
     by (simp add: power2_sum)
   have "2*(t+u)*(s+v) =  2*t * s + 2*t * v +2*u * s +2*u * v"
     using int_distrib(1) int_distrib(2) by force
   from this b_simp1 have b_expression:"b^2 = t^2+u^2+s^2+v^2+2*t*u+2 * s * v + 
 2*t * s + 2*t * v +2*u * s +2*u * v" by auto
   thus ?thesis by auto
 qed
 
 lemma four_terms_bin_exp_twodiff:
   fixes b s t u v :: int
   assumes "b = s+t-u-v"
   shows "b^2 =  t^2+u^2+s^2+v^2-2*t*u-2 * s * v + 2*t * s - 2*t * v -2*u * s +2*u * v"
 
 proof -
   from assms have "b^2 = (s-u)^2+(t-v)^2+2*(s-u)*(t-v)" by (smt (verit, best) power2_sum) 
   hence b_simp1:"b^2 = s^2+u^2-2 * s *u + t^2+v^2 - 2 * t * v + 2*(s-u)*(t-v)"
     by (simp add: power2_diff)
   have "2*(s-u)*(t-v) = 2* s * t - 2* s * v - 2*u*t+2*u * v" 
     by (simp add: Rings.ring_distribs(3) Rings.ring_distribs(4))
   from this b_simp1 have b_expression: "b^2 =  t^2+u^2+s^2+v^2-2*t*u-2 * s * v + 
 2*t * s - 2*t * v -2*u * s +2*u * v" by auto
   thus ?thesis by auto
 qed
 
 text\<open>If a quadratic with positive leading coefficient is always non-negative, its discriminant is
 non-positive.\<close>
 
 lemma qua_disc:
   fixes a b c :: real
   assumes "a>0"
   assumes "\<forall>x::real. a*x^2+b*x+c \<ge>0"
   shows "b^2 - 4*a*c \<le> 0"
 
 proof -
   from assms have 0:"\<forall>x::real. (a*x^2+b*x+c)/a \<ge>0" by simp
   from assms have 1:"\<forall>x::real.(b*x+c)/a = b/a*x+c/a" by (simp add: add_divide_distrib)
   from assms have "\<forall>x::real.(a*x^2+b*x+c)/a = x^2+(b*x+c)/a" by (simp add: is_num_normalize(1))
   from 1 this have "\<forall>x::real.(a*x^2+b*x+c)/a = x^2+b/a*x+c/a" by simp
   hence atleastzero:"\<forall>x::real. x^2+b/a*x+c/a \<ge>0" using 0 by simp
 
   from assms have 2:"\<forall>x::real. x^2+b/a*x+c/a = x^2+2*b/(2*a)*x+c/a+b^2/(4*a^2)-b^2/(4*a^2)" by simp
   have simp1:"\<forall>x::real.(x+b/(2*a))^2 = x^2+2*b/(2*a)*x+(b/(2*a))^2" by (simp add: power2_sum)
   have "(b/(2*a))^2 = b^2/(4*a^2)" by (metis four_x_squared power_divide)
   hence "\<forall>x::real. x^2+b/a*x+c/a = (x+b/(2*a))^2+c/a-b^2/(4*a^2)" using 2 simp1 by auto
   hence "\<forall>x::real. (x+b/(2*a))^2+c/a-b^2/(4*a^2) \<ge>0" using atleastzero by presburger
   hence 3:"\<forall>x::real. b^2/(4*a^2)-c/a\<le>(x+b/(2*a))^2" by (smt (verit, del_insts))
   have "\<exists>x::real. (x+b/(2*a))^2=0" by (metis diff_add_cancel power_zero_numeral)
   hence "b^2/(4*a^2)-c/a\<le>0" using 3 by metis
   hence 4:"4*a^2*(b^2/(4*a^2)-c/a)\<le>0" using assms by (simp add: mult_nonneg_nonpos)
   have 5:"4*a^2*b^2/(4*a^2) = b^2" using assms by simp
   have 6:"4*a^2*c/a = 4*a*c" using assms by (simp add: power2_eq_square)
   show ?thesis using 4 5 6 assms by (simp add: Rings.ring_distribs(4))
 qed
 
 text\<open>The following lemma shows for any point on a 3D sphere with radius $a$, the sum of its coordinates 
 lies between $\sqrt{3a}$ and $-\sqrt{3a}$.\<close>
 
 lemma three_terms_Cauchy_Schwarz:
   fixes x y z a :: real
   assumes "a > 0"
   assumes "x^2+y^2+z^2 = a"
   shows "(x+y+z)\<ge>-sqrt(3*a) \<and> (x+y+z)\<le>sqrt(3*a)"
 
 proof -
   have 1:"\<forall>t::real. (t*x+1)^2 = t^2*x^2+1+2*t*x" by (simp add: power2_sum power_mult_distrib)
   have 2:"\<forall>t::real. (t*y+1)^2 = t^2*y^2+1+2*t*y" by (simp add: power2_sum power_mult_distrib)
   have 3:"\<forall>t::real. (t*z+1)^2 = t^2*z^2+1+2*t*z" by (simp add: power2_sum power_mult_distrib)
   from 1 2 3 have 4:"\<forall>t::real.(t*x+1)^2+(t*y+1)^2+(t*z+1)^2 = t^2*x^2+1+2*t*x + t^2*y^2+1+2*t*y +
 t^2*z^2+1+2*t*z" by auto
 
   have "\<forall>t::real. t^2*x^2+t^2*y^2=t^2*(x^2+y^2)" by (simp add: nat_distrib(2))
   hence 5:"\<forall>t::real. t^2*x^2+t^2*y^2+t^2*z^2=t^2*(x^2+y^2+z^2)" by (metis nat_distrib(2))
   have 6:"\<forall>t::real. 2*t*x+2*t*y+2*t*z = t*2*(x+y+z)" by (simp add: Groups.mult_ac(2) distrib_right)
   from 4 5 6 have "\<forall>t::real.(t*x+1)^2+(t*y+1)^2+(t*z+1)^2 = t^2*(x^2+y^2+z^2)+ t*2*(x+y+z)+3" 
     by (smt (verit, best))
   hence "\<forall>t::real. t^2*(x^2+y^2+z^2)+ t*2*(x+y+z)+3 \<ge>0" by (metis add_nonneg_nonneg zero_le_power2)
   hence "(2*(x+y+z))^2 - 12*(x^2+y^2+z^2)\<le>0" using qua_disc
     by (smt (z3) power2_diff power2_sum power_zero_numeral sum_squares_bound)
   hence "12*(x^2+y^2+z^2)\<ge>4*(x+y+z)^2" by (simp add: four_x_squared)
   hence "3*a\<ge>(x+y+z)^2" using assms by auto
   thus ?thesis by (smt (verit, del_insts) real_sqrt_abs real_sqrt_le_iff)
 qed
 
 text\<open>We adapt the lemma above through changing the types for the convenience of our proof.\<close>
 
 lemma three_terms_Cauchy_Schwarz_nat_ver:
   fixes x y z a :: nat
   assumes "a>0"
   assumes "x^2+y^2+z^2 = a"
   shows "(x+y+z)\<ge>-sqrt(3*a) \<and> (x+y+z)\<le>sqrt(3*a)"
 
 proof -
   have fac1:"real(x+y+z) = real x + real y + real z" by auto
   have fac2: "3*(real a) = real(3*a)" by auto
   thus ?thesis using fac1 three_terms_Cauchy_Schwarz fac2 by (smt (verit) assms(1) assms(2) nat_less_real_le of_nat_0_le_iff of_nat_add of_nat_power)
 qed
 
 text\<open>This theorem is Lemma 1.12 in \cite{nathanson1996}, which shows for odd positive integers $a$ and $b$ 
 satisfying certain properties, there exist four non-negative integers $s,t,u$ and $v$ such that 
 $a = s^2+t^2+u^2+v^2$ and $b = s+t+u+v$. We use the Three Squares Theorem AFP entry \cite{Three_Squares-AFP}.\<close>
 
 theorem four_nonneg_int_sum:
   fixes a b :: nat
   assumes "a\<ge>1"
   assumes "b\<ge>1"
   assumes "odd a"
   assumes "odd b"
   assumes 3:"b^2 < 4*a"
   assumes "3*a < b^2+2*b+4"
   shows "\<exists>s t u v :: int. s \<ge> 0 \<and> t \<ge> 0 \<and> u \<ge> 0 \<and> v \<ge> 0 \<and> a = s^2 + t^2 + u^2 + v^2 \<and>
  b = s+t+u+v"
 
 proof -
   from assms have 0:"\<exists>k1 :: nat. a = 2*k1+1" by (meson oddE)
   from assms have 1:"\<exists>k2 :: nat. b = 2*k2+1" by (meson oddE)
   from 0 have "4*a mod 8 = 4" by auto
   hence 2:"8 dvd (4*a-4)" by (metis dvd_minus_mod)
 
   obtain k2 where "b = 2*k2+1" using 1 by auto
   have "2 dvd k2*(k2+1)" by auto
   hence "8 dvd 4*k2*(k2+1)" by (metis ab_semigroup_mult_class.mult_ac(1) 
         mult_2_right nat_mult_dvd_cancel_disj numeral_Bit0)
   hence "b^2 mod 8 = 1" using 1 by (metis One_nat_def Suc_0_mod_numeral(2) assms(4)
         square_mod_8_eq_1_iff unique_euclidean_semiring_class.cong_def)
   hence "8 dvd (b^2-1)" by (metis dvd_minus_mod)
   from 2 this have "8 dvd ((4*a-4)-(b^2-1))" using dvd_diff_nat by blast
   from assms 0 1 and this have 7:"8 dvd ((4*a-b^2)-3)" by auto
   from assms 0 1 have 5:"4*a-b^2\<noteq>1" using not_one by auto
   from assms 0 1 have 6:"4*a-b^2\<noteq>2" using not_two by auto
   from 3 5 6 have "4*a-b^2 \<ge> 3" by auto
   from this 7 have 8:"(4*a-b^2) mod 8 = 3" using mod_nat_eqI by presburger
 
   obtain j k l where ints:"odd j \<and> odd k \<and> odd l \<and> (4*a-b^2) = j^2+k^2+l^2"
     using 8 odd_three_squares_using_mod_eight by presburger
   define x where "x = sort[j,k,l] ! 2"
   define y where "y = sort[j,k,l] ! 1"
   define z where "z = sort[j,k,l] ! 0"
 
   have "x^2+y^2+z^2 = sum_list (map (\<lambda>x. x^2) [j,k,l])" using x_def y_def z_def by auto
   from this ints have a_and_b:"(4*a-b^2) = x^2+y^2+z^2" by auto
 
   have size:"x\<ge>y \<and> y\<ge>z" using x_def y_def z_def by auto
   have x_par:"x = j \<or> x = k \<or> x = l" using x_def by auto
   have y_par:"y = j \<or> y = k \<or> y = l" using y_def by auto
   have z_par:"z = j \<or> z = k \<or> z = l" using z_def by auto
   hence parity:"odd x \<and> odd y \<and> odd z" using ints x_par y_par z_par by fastforce
   from "1" have b_par:"odd b" by auto
 
   obtain w::int where w_def:"(w=z \<or> w=-z) \<and> (b+x+y+w) mod 4 = 0" (*This is the \pm z in proof*)
     using suit_z size parity b_par by presburger
 
   from parity have fac1:"(int z) mod 4 = 3 \<or> (int z) mod 4 = 1" by presburger
   from parity have fac2:"-z mod 4 = 3 \<or> -z mod 4 = 1" by presburger
   from w_def have fac3:"w mod 4 = 3 \<or> w mod 4 = 1" using fac1 fac2 by auto
 
   have s_int:"4 dvd (b+x+y+w)" using b_par parity fac3 w_def by presburger
   have b_x_int:"2 dvd (b+x)" using b_par parity by presburger
   have b_y_int:"2 dvd (b+y)" using b_par parity by presburger
   have b_w_int:"2 dvd (b+w)" using b_par fac3 by presburger
 
   obtain s::int where s_def:"s = (b+x+y+w) div 4" using s_int by fastforce
   obtain t::int where t_def:"t = (b+x) div 2 - s" using s_int b_x_int by blast
   obtain u::int where u_def:"u = (b+y) div 2 - s" using s_int b_y_int by blast
   obtain v::int where v_def:"v = (b+w) div 2 - s" using s_int b_w_int by blast
 
   from t_def s_def have t_simp1:"t = (2*b+2*x) div 4 - (b+x+y+w) div 4" by auto
   have t_simp2:"(2* b+2* x) - (b+x+y+w) = b+x-y-w" using size by auto
   hence t_expre:"t = (b+x-y-w) div 4" using t_simp1 by (smt (verit, ccfv_SIG) add_num_simps(1) 
 div_plus_div_distrib_dvd_right numeral_Bit0 of_nat_numeral one_plus_numeral s_int 
-unique_euclidean_semiring_with_nat_class.of_nat_div)
+linordered_euclidean_semiring_class.of_nat_div)
   from b_x_int have "4 dvd (2*b+2*x)"
     by (metis distrib_left_numeral mult_2_right nat_mult_dvd_cancel_disj numeral_Bit0)
   hence four_div_tn:"4 dvd (b+x-y-w)" using s_int t_simp2 by presburger
 
   have " (b+x) div 2 +  (b+y) div 2 = (2*b+x+y) div 2"
     by (smt (verit, best) Groups.add_ac(2) b_y_int div_plus_div_distrib_dvd_right 
 left_add_twice nat_arith.add2)
   hence threesum:"t + u + s = (2*b+x+y) div 2 - s" using t_def u_def by auto
 
   have "2 dvd (x+y)" using parity by auto
   hence "(2*b+x+y) div 2 + (b+w) div 2 = (2*b+b+x+y+w) div 2"
     by (smt (verit, ccfv_threshold) Num.of_nat_simps(4) b_w_int div_plus_div_distrib_dvd_right
  landau_product_preprocess(4) numerals(1) of_nat_1 one_plus_numeral
- unique_euclidean_semiring_with_nat_class.of_nat_div)
+ linordered_euclidean_semiring_class.of_nat_div)
 
   hence "t+u+s+v = (2*b+b+x+y+w) div 2 -s -s" using v_def threesum by auto
   hence foursum0:"t+u+s+v = (2*b+b+x+y+w) div 2 - (b+x+y+w) div 4 - (b+x+y+w) div 4" 
     using s_def by auto
   have foursum1:"(b+x+y+w) div 4 + (b+x+y+w) div 4 = (b+x+y+w) div 2" 
     using div_mult_swap s_int by auto
   have "(2*b+b+x+y+w) div 2 - (b+x+y+w) div 2 = (2*b) div 2" by auto
   hence "t+u+s+v = (2*b) div 2" using foursum0 foursum1 by linarith
   hence second:"t+u+s+v = b" by auto
 
   from a_and_b have "4*a = x^2+y^2+z^2+b^2"
     by (metis Nat.add_diff_assoc2 add_diff_cancel_right' assms(5) less_or_eq_imp_le)
   hence "a = (x^2+y^2+z^2+b^2) div 4" using parity b_par by auto
 
   from second have b_expresion:"b^2 = t^2+u^2+s^2+v^2+2*t*u+2* s * v + 
 2*t* s + 2*t * v +2*u * s +2*u * v" using four_terms_bin_exp_allsum
     by (metis is_num_normalize(1) nat_arith.add2 of_nat_power)
 
   define sn where sn_def:"sn = b+x+y+w" (*Numerator of s*)
   from sn_def s_def have sn_nume: "4* s = sn" by (metis dvd_div_mult_self mult.commute s_int)
   from sn_def have sn_sqr:"sn^2 = b^2+x^2+y^2+w^2+2* b * x+2* b * y+2*b*w+2*x*y+2*x*w+2*y*w" 
     using four_terms_bin_exp_allsum w_def by auto
   hence s_pen:"16* s^2 = b^2+x^2+y^2+w^2+2*b*x+2*b*y+2*b*w+2*x*y+2*x*w+2*y*w" using sn_nume by auto
   have "4 dvd sn" using s_int sn_def by auto
   hence "16 dvd sn^2" by auto
   hence s_sqr_expression:"s^2=(b^2+x^2+y^2+w^2+2*b*x+2*b*y+2*b*w+2*x*y+2*x*w+2*y*w) div 16" 
     using sn_sqr s_pen by auto
 
   define tn where tn_def:"tn = b+x-y-w" (*Numerator of t*)
   from tn_def t_expre size four_div_tn have tn_nume: "4* t = tn"
     by (metis dvd_div_mult_self mult.commute)
   from size assms have "b+x-y > 0" by auto
   hence "tn = int b + int x - int y -w" using tn_def by auto
   from this have tn_sqr:"tn^2 = b^2+x^2+y^2+w^2+2*b*x-2*b*y-2*b*w-2*x*y-2*x*w+2*y*w"
     using four_terms_bin_exp_twodiff w_def by auto
   hence t_pen:"16*t^2 = b^2+x^2+y^2+w^2+2*b*x-2*b*y-2*b*w-2*x*y-2*x*w+2*y*w" using tn_nume by auto
   have "16 dvd tn^2" using tn_def four_div_tn by auto
   hence t_sqr_expression:"t^2=(b^2+x^2+y^2+w^2+2*b*x-2*b*y-2*b*w-2*x*y-2*x*w+2*y*w) div 16"
     using tn_sqr t_pen by auto
  
   from size s_def t_expre w_def have sgeqt:"s\<ge>t" by auto
   from size s_def t_def u_def have tgequ:"t\<ge>u" by auto
   from size s_def u_def v_def w_def have ugeqv:"u\<ge>v" by auto
 
   from assms(6) have "12*a < 4*b^2+8*b+16" by auto
   hence "12*a-3*b^2 < b^2+8*b+16" by auto
   hence "12*a-3*b^2 < (b+4)^2" 
     by (smt (z3) add.commute add.left_commute mult_2 numeral_Bit0 power2_eq_square power2_sum)
   hence mid_ineq:"sqrt(12*a-3*b^2) < b+4" 
     by (meson of_nat_0_le_iff of_nat_power_less_of_nat_cancel_iff real_less_lsqrt)
 
   define ab::nat where ab_def:"ab = 4*a-b^2"
   from assms ab_def have nonneg_ab:"ab>0" by auto
   from a_and_b ab_def have sum_of_sqrs:"x^2+y^2+z^2 = ab" by auto
   from this nonneg_ab have "x^2+y^2+z^2>0" by auto
   from this sum_of_sqrs three_terms_Cauchy_Schwarz_nat_ver have "x+y+z \<le> sqrt(3*ab)" by auto
   hence left_ineq:"x+y+z \<le> sqrt(3*(4*a-b^2))" using ab_def by auto
   have "sqrt(3*(4*a-b^2)) = sqrt(12*a-3*b^2)" by (simp add: diff_mult_distrib2)
   from left_ineq mid_ineq this have "x+y+z < b+4" by auto
   hence num_bound:"int b- x- y- z > -4" by auto
 
   define vn where vn_def:"vn = int b+w-x-y"
   from num_bound vn_def w_def have vn_bound:"vn > -4" by auto
   from w_def have four_div_sn:"4 dvd (int b +x+y+w)" by auto
   from parity have "4 dvd (int 2*x+2*y)" 
     by (metis Num.of_nat_simps(5) \<open>even (x + y)\<close> distrib_left int_dvd_int_iff 
 nat_mult_dvd_cancel_disj num_double numeral_mult of_nat_add of_nat_numeral)
   hence "4 dvd (int b +x+y+w - 2*x - 2*y)" using four_div_sn
     by (smt (verit) Num.of_nat_simps(5) dvd_add_left_iff)
   hence "4 dvd vn" using vn_def by presburger
 
   from v_def s_def have "v = (int 2*b + 2*w) div 4 - (int b + x + y + w) div 4" by auto
   hence v_expre:"v = (int b-x-y+w) div 4" using four_div_sn by fastforce
   hence "v = vn div 4" using vn_def by auto
   hence "v \<ge> 0" using vn_bound four_div_sn using \<open>4 dvd vn\<close> by fastforce
   hence stuv_nonneg:" s \<ge> 0 \<and> t \<ge> 0 \<and> u \<ge> 0 \<and> v \<ge> 0 " using sgeqt tgequ ugeqv by linarith
 
   from vn_def have vn_sqr:"vn^2 = b^2+x^2+y^2+w^2 - 2*b*x-2*b*y+2*b*w+2*x*y-2*x*w-2*y*w" 
     using four_terms_bin_exp_twodiff w_def by auto
   from \<open>v = vn div 4\<close> have vn_is_num:"v^2 = vn^2 div 16" using \<open>4 dvd vn\<close> by fastforce
   hence "16 dvd vn^2" using v_def using \<open>4 dvd vn\<close> by fastforce
   from vn_is_num vn_sqr have 
   v_sqr_expression:"v^2=(b^2+x^2+y^2+w^2-2*b*x-2*b*y+2*b*w+2*x*y-2*x*w-2*y*w) div 16" by auto
   
   define un where un_def:"un = int b+y-x-w"
   from parity w_def have "even (x+w)" by auto
   from this parity have "4 dvd (int 2*x+2*w)" 
     by (metis distrib_left even_numeral mult_2_right mult_dvd_mono numeral_Bit0 of_nat_numeral)
   hence "4 dvd (int b +x+y+w - 2*x-2*w)" using four_div_sn
     by (smt (verit) Num.of_nat_simps(5) dvd_add_left_iff)
   hence "4 dvd un" using un_def by presburger
 
   from u_def s_def have "u = (int 2*b+2*y) div 4 - (int b + x + y + w) div 4" by auto
   hence u_expre:"u = (int b-x+y-w) div 4" using four_div_sn by fastforce
   hence "u = un div 4" using un_def by auto
   from un_def have un_sqr:"un^2 = b^2+x^2+y^2+w^2+2*b*y-2*b*x-2*b*w-2*y*x-2*y*w+2*x*w"
     using four_terms_bin_exp_twodiff w_def by auto
   from \<open>u = un div 4\<close> have un_is_num:"u^2 = un^2 div 16" using \<open>4 dvd un\<close> by fastforce
   hence "16 dvd un^2" using u_def using \<open>4 dvd un\<close> by fastforce
   from un_is_num un_sqr have
   u_sqr_expression:"u^2 = (b^2+x^2+y^2+w^2+2*b*y-2*b*x-2*b*w-2*y*x-2*y*w+2*x*w) div 16" by auto
   
   from u_sqr_expression v_sqr_expression have
   uv_simp1:"u^2+v^2 = (int b^2+x^2+y^2+w^2-2*b*x-2*b*y+2*b*w+2*x*y-2*x*w-2*y*w) div 16 + 
   (int b^2+x^2+y^2+w^2+2*b*y-2*b*x-2*b*w-2*y*x-2*y*w+2*x*w) div 16" by auto
   have uv_simp2:"(int b^2+x^2+y^2+w^2-2*b*x-2*b*y+2*b*w+2*x*y-2*x*w-2*y*w)+
   (int b^2+x^2+y^2+w^2+2*b*y-2*b*x-2*b*w-2*y*x-2*y*w+2*x*w)=
   (int 2*b^2+2*x^2+2*y^2+2*w^2-4*b*x-4*y*w)" by auto
   hence "16 dvd (int 2*b^2+2*x^2+2*y^2+2*w^2-4*b*x-4*y*w)" by (smt (verit) \<open>16 dvd un\<^sup>2\<close> \<open>16 dvd vn\<^sup>2\<close>
  dvd_add_right_iff of_nat_power un_sqr vn_sqr zadd_int_left)
   hence usqr_plus_vsqr:"u^2+v^2 = (int 2*b^2+2*x^2+2*y^2+2*w^2-4*b*x-4*y*w) div 16" 
     using uv_simp1 uv_simp2 by (smt (verit, ccfv_threshold) Num.of_nat_simps(4) Num.of_nat_simps(5)
  \<open>16 dvd vn\<^sup>2\<close> div_plus_div_distrib_dvd_right power2_eq_square vn_sqr)
 
   have allsum0:"s^2+t^2+u^2+v^2 = (sn^2+tn^2+un^2+vn^2) div 16" using \<open>16 dvd vn\<^sup>2\<close> \<open>16 dvd sn\<^sup>2\<close> 
 \<open>16 dvd un\<^sup>2\<close> \<open>16 dvd tn\<^sup>2\<close> s_sqr_expression t_sqr_expression u_sqr_expression v_sqr_expression
 sn_sqr tn_sqr un_sqr vn_sqr by (metis add.commute div_plus_div_distrib_dvd_left)
   have allsum1:"(sn^2+tn^2+un^2+vn^2) = (int 4*b^2+4*x^2+4*y^2+4*w^2)" 
     using sn_sqr tn_sqr un_sqr vn_sqr by auto
   have "16 dvd (sn^2+tn^2+un^2+vn^2)" 
     by (simp add: \<open>16 dvd sn\<^sup>2\<close> \<open>16 dvd tn\<^sup>2\<close> \<open>16 dvd un\<^sup>2\<close> \<open>16 dvd vn\<^sup>2\<close>) 
   hence "16 dvd 4*(int b^2+x^2+y^2+w^2)" using allsum1 by auto
   hence "4 dvd (int b^2+x^2+y^2+w^2)" by presburger
   from allsum1 have "s^2+t^2+u^2+v^2 = (int 4*b^2+4*x^2+4*y^2+4*w^2) div 16" 
     using allsum0 by presburger
   hence "s^2+t^2+u^2+v^2 = 4*(int b^2+x^2+y^2+w^2) div 16" by simp
   hence allsum2:"s^2+t^2+u^2+v^2 = (int b^2+x^2+y^2+w^2) div 4" by simp
 
   from a_and_b have "4*a = int b^2+x^2+y^2+w^2" using w_def
     using \<open>4 * a = x\<^sup>2 + y\<^sup>2 + z\<^sup>2 + b\<^sup>2\<close> by fastforce
   hence first:"a = s^2+t^2+u^2+v^2" using allsum2 by linarith
 
   show ?thesis using first second stuv_nonneg by (smt (verit, best))
 qed
 end
\ No newline at end of file