Theory DFI_square_2

theory DFI_square_2
  imports DFI_square_1 HOL.NthRoot
begin

lemma sun_lemma10_rec:
  fixes A::int and n::int and t::int and k::int
  assumes "A > 2" and "n > 3" and "χ_int A n = 2*k"
  shows "(s mod (4*n) = t mod (4*n) ∨ (s+t) mod (4*n) = (2*n) mod (4*n))
      ⟹ (ψ_int A s mod k = ψ_int A t mod k)"
proof -
  have rec1: "(s+t) mod (4*n) = (2*n) mod (4*n) ⟹ ψ_int A s mod k = ψ_int A t mod k"
  proof -
    assume s_plus_t: "(s+t) mod (4*n) = (2*n) mod (4*n)"
    hence s_plus_t_2: "(s+t-2*n) mod (4*n) = 0 mod (4*n)"
      using mod_diff_cong[of "s+t" "4*n" "2*n" "2*n" "2*n"]  by auto
    hence s_plus_t_3: "(4*n) dvd (s+t-2*n)" by auto
    obtain q where q_def: "(s+t-2*n) = (4*n)*q" using s_plus_t_3
      by blast
    have "ψ_int A s mod k= ψ_int A (4*n*q + 2*n-t) mod k" using q_def by (smt (verit))
    hence "ψ_int A s mod k = ψ_int A (2*n-t) mod k"
      using technical_lemma2[of n A k q] assms by (smt (z3))
    hence "ψ_int A s mod k = (- ψ_int A (-t)) mod k"
      using assms technical_cor3[of n A k "-t"] by auto
    thus "ψ_int A s mod k = ψ_int A t mod k" using ψ_int_odd by auto
  qed
  have rec2: "s mod (4*n) = t mod (4*n) ⟹ ψ_int A s mod k = ψ_int A t mod k"
  proof -
    assume s_eq_t: "s mod (4*n) = t mod (4*n)"
    obtain q where q_def: "s = 4*n*q + t" using s_eq_t by (smt (verit, ccfv_SIG) mod_eqE)
    thus "ψ_int A s mod k = ψ_int A t mod k" using q_def technical_lemma2[of n A k q] assms by auto
  qed
  show "(s mod (4*n) = t mod (4*n) ∨ (s+t) mod (4*n) = (2*n) mod (4*n))
      ⟹ (ψ_int A s mod k = ψ_int A t mod k)"  using rec1 rec2 by blast
qed

text ‹Some results about Lucas sequences seen as real numbers›

lemma expr_of_ψ_and_χ:
  fixes A::int and n::nat and α::real
  assumes "A > 2" and "α^2 = A^2-4" and "α > 0"
  defines "βp ≡ (A+α) / 2" and "βm ≡ (A-α) / 2"
  shows "real_of_int (ψ A n) = (βp^n-βm^n) / α ∧
real_of_int (χ A n) = βp^n+βm^n"
proof (induction n rule: ψ_induct)
  case 0
  then show ?case by auto
next
  case 1
  have "βp^1-βm^1 = βp - βm" by (auto simp add: algebra_simps)
  hence "βp^1-βm^1 = α" using βp_def βm_def
    by (metis add.commute add_right_cancel diff_add_cancel real_average_minus_first)
  hence "(βp^1-βm^1) / α = 1 ∧ real_of_int (ψ A 1) = 1" using assms by auto
  hence part_ψ: "real_of_int (ψ A 1) = (βp^1-βm^1) / α" by metis
  have "βp^1+βm^1 = real_of_int A" unfolding βp_def βm_def
    by (smt (z3) field_sum_of_halves power_one_right)
  then show ?case using part_ψ by auto
next
  case (sucsuc n)
  note t = this
  have βp_eq: "A*βp-1 = βp^2"
  proof -
    have "βp^2 = (A+α)*(A+α)/4" unfolding βp_def using power2_eq_square[of "(A+α) / 2"] by auto
    hence "βp^2 = (A^2+2*A*α+α^2)/4" by (auto simp add: power2_eq_square algebra_simps)
    hence "βp^2 = (A^2 + A*α - 2)/2" using assms(2) by (auto simp add: algebra_simps)
    hence "βp^2 = A*(A+α)/2 - 1" using power2_eq_square[of A]
      by (auto simp add: algebra_simps diff_divide_distrib)
    thus ?thesis using βp_def by auto
  qed
  have βm_eq: "A*βm-1 = βm^2"
  proof -
    have "βm^2 = (A-α)*(A-α)/4" unfolding βm_def using power2_eq_square[of "(A-α) / 2"] by auto
    hence "βm^2 = (A^2-2*A*α+α^2)/4" by (auto simp add: power2_eq_square algebra_simps)
    hence "βm^2 = (A^2 - A*α - 2)/2" using assms(2) by (auto simp add: algebra_simps)
    hence "βm^2 = (A*(A-α) - 2)/2" by (auto simp add: algebra_simps power2_eq_square)
    hence "βm^2 = (A*(A-α))/2 - 1" by (auto simp add: diff_divide_distrib)
    hence "βm^2 = A*(A-α)/2 - 1" by auto
    thus ?thesis using βm_def by auto
  qed
  have "real_of_int (ψ A (Suc (Suc n))) =  A * (βp^(Suc n)-βm^(Suc n)) / α - (βp^n-βm^n) / α"
    using t by auto
  hence "real_of_int (ψ A (Suc (Suc n))) = (A * (βp*βp^n-βm*βm^n)) / α - (βp^n-βm^n) / α"
    by simp
  hence "real_of_int (ψ A (Suc (Suc n))) = (A * (βp*βp^n-βm*βm^n) - (βp^n-βm^n)) / α"
    using assms by (smt (verit, ccfv_SIG) add_divide_distrib)
  hence "real_of_int (ψ A (Suc (Suc n))) = ((A*βp-1)*βp^n - (A*βm-1)*βm^n) / α"
    by (auto simp add: algebra_simps)
  hence "real_of_int (ψ A (Suc (Suc n))) = (βp^2*βp^n - βm^2*βm^n)/α" using βp_eq βm_eq by auto
  hence form_ψ: "real_of_int (ψ A (Suc (Suc n))) = (βp^(Suc (Suc n))-βm^(Suc (Suc n))) / α"
    using power_add[of βp 2 n] power_add[of βm 2 n] by (metis add_2_eq_Suc)

  have "real_of_int (χ A (Suc (Suc n))) =  A * (βp^(Suc n)+βm^(Suc n)) - (βp^n+βm^n)"
    using t by auto
  hence "real_of_int (χ A (Suc (Suc n))) = (A * (βp*βp^n+βm*βm^n)) - (βp^n+βm^n)"
    by simp
  hence "real_of_int (χ A (Suc (Suc n))) = (A*βp-1)*βp^n + (A*βm-1)*βm^n"
    by (auto simp add: algebra_simps)
  hence "real_of_int (χ A (Suc (Suc n))) = βp^2*βp^n + βm^2*βm^n" using βp_eq βm_eq by auto
  hence form_χ: "real_of_int (χ A (Suc (Suc n))) = βp^(Suc (Suc n))+βm^(Suc (Suc n))"
    using power_add[of βp 2 n] power_add[of βm 2 n] by (metis add_2_eq_Suc)
  then show ?case using form_ψ form_χ by auto
qed

lemma χ_is_Bigger_sqrt5ψ: "A > 2 ⟹ χ A n > sqrt 5*ψ A n"
proof (cases n)
  case 0
  then show ?thesis by auto
next
  case (Suc k)
  note t = this
  assume A_def: "A > 2"
  hence "A ≥ 3" by simp
  hence "A*A ≥ 9" using mult_mono[of 3 A 3 A] A_def by auto
  hence DiscB4: "A^2-4 ≥ 5" using power2_eq_square[of A] by auto
  define α where "α = sqrt(A^2-4)"
  have α_def2: "α^2 = A^2 - 4"
    unfolding α_def using DiscB4 of_int_0_le_iff real_sqrt_pow2 by fastforce
  hence αB2: "α ≥ sqrt 5"
    using DiscB4 apply simp by (metis DiscB4 α_def of_int_le_iff of_int_numeral real_sqrt_le_iff)
  hence α_pos: "α > 0"
    by (meson not_numeral_le_zero order.trans real_sqrt_le_0_iff verit_comp_simplify1(3))
  define βp where "βp = (A+α)/2"
  define βm where "βm = (A-α)/2"
  have "α^2 < A^2" using α_def2 by auto
  hence "α < A" using real_sqrt_less_iff[of "α^2" "A^2"] A_def αB2 by auto
  hence "βm > 0" using βm_def by simp
  hence βm_pos: "βm^n > 0" by auto
  have "χ A n = βp^n+βm^n"
    unfolding βp_def βm_def using expr_of_ψ_and_χ[of A α n] α_def2 A_def α_pos by simp
  hence "χ A n > βp^n - βm^n"
    using βm_pos diff_mono[of "βp^n+βm^n" "βp^n+βm^n" "2*βm^n" 0] by linarith
  hence "χ A n > α * ((βp^n - βm^n)/ α)" using αB2 by auto
  hence "χ A n > α * ψ A n"
    unfolding βp_def βm_def using expr_of_ψ_and_χ[of A α n] α_def2 A_def α_pos by simp
  hence "χ A n > sqrt 5* ψ A n"
    using lucas_strict_monotonicity[of A k] t A_def αB2 mult_left_mono[of "sqrt 5" α "ψ A n"]
    by (smt (z3) mult_of_int_commute of_int_0_less_iff)
  then show ?thesis by auto
qed

lemma χ_is_Bigger_2ψ: "A > 2 ⟹ χ A n > 2*ψ A n"
proof -
  assume A_def: "A > 2"
  have ineq: "sqrt 5 > 2"
    by (metis numeral_less_iff order_refl real_sqrt_four real_sqrt_less_iff semiring_norm(79))
  have "χ A n > sqrt 5 * ψ A n" using χ_is_Bigger_sqrt5ψ A_def by auto
  thus ?thesis using ineq mult_right_mono[of 2 "sqrt 5" "ψ A n"] A_def
    using lucas_monotone2[of A "0" n] by auto
qed

lemma ψ_ineq_opti:
  fixes A::int and n::nat
  assumes "A > 2"
  shows "5* ψ A n < 2*ψ A (n+1)"
proof -
  have "A ≥ 3" using assms by simp
  hence "A*A ≥ 9" using mult_mono[of 3 A 3 A] assms by auto
  hence DiscB4: "A^2-4 > 4" using power2_eq_square[of A] by auto
  define α where "α = sqrt(A^2-4)"
  have α_def2: "α^2 = A^2 - 4"
    unfolding α_def using DiscB4 using of_int_0_le_iff real_sqrt_pow2 by fastforce
  hence αB2: "α > 2"
    using DiscB4 by (metis α_def of_int_less_iff of_int_numeral real_sqrt_four real_sqrt_less_iff)
  define βp where "βp = (A+α)/2"
  define βm where "βm = (A-α)/2"
  have "α^2 < A^2" using α_def2 by auto
  hence "α < A" using real_sqrt_less_iff[of "α^2" "A^2"] assms αB2 by auto
  hence "βm > 0" using βm_def by simp
  hence βm_pos: "βm^n > 0" by auto
  have βpB2: "βp > 5/2" unfolding βp_def using assms αB2 by auto
  have "ψ A (n+1) = (βp^(n+1) - βm^(n+1))/ α"
    using expr_of_ψ_and_χ[of A α "n+1"] assms α_def2 αB2 βp_def βm_def by fastforce
  hence "ψ A (n+1) = ((βp*βp^n - βp*βm^n) + (βp*βm^n - βm*βm^n))/ α"
    using power_Suc[of βp n] power_Suc[of βm n] by simp
  hence "ψ A (n+1) = (βp*βp^n - βp*βm^n)/ α + (βp*βm^n - βm*βm^n)/ α"
    using add_divide_distrib[of "(βp*βp^n - βp*βm^n)" "(βp*βm^n - βm*βm^n)" α] assms by simp
  hence "ψ A (n+1) = βp*(βp^n-βm^n)/ α + βm^n*(βp-βm)/ α" by (auto simp add: algebra_simps)
  hence "ψ A (n+1) = βp*ψ A n + βm^n*(βp-βm)/ α"
    using βp_def βm_def expr_of_ψ_and_χ[of A α n] α_def2 αB2 assms by fastforce
  hence "ψ A (n+1) = βp*ψ A n + βm^n"
    using βp_def βm_def diff_divide_distrib[of "A+α" "A-α" 2] αB2 apply simp by (simp add: βm_def)
  hence "ψ A (n+1) > βp * ψ A n" using βm_pos by auto
  thus ?thesis using βpB2 using lucas_monotone2[of A "0" n] assms mult_right_mono[of "5/2" βp "ψ A n"] by auto
qed

lemma ψ_doubles:
  fixes A::int and n::nat
  assumes "A > 2"
  shows "2*ψ A n < ψ A (n+1)"
proof -
  have "A ≥ 3" using assms by simp
  hence "A*A ≥ 9" using mult_mono[of 3 A 3 A] assms by auto
  hence DiscB4: "A^2-4 > 4" using power2_eq_square[of A] by auto
  define α where "α = sqrt(A^2-4)"
  have α_def2: "α^2 = A^2 - 4"
    unfolding α_def using DiscB4 using of_int_0_le_iff real_sqrt_pow2 by fastforce
  hence αB2: "α > 2"
    using DiscB4 by (metis α_def of_int_less_iff of_int_numeral real_sqrt_four real_sqrt_less_iff)
  define βp where "βp = (A+α)/2"
  define βm where "βm = (A-α)/2"
  have "α^2 < A^2" using α_def2 by auto
  hence "α < A" using real_sqrt_less_iff[of "α^2" "A^2"] assms αB2 by auto
  hence "βm > 0" using βm_def by simp
  hence βm_pos: "βm^n > 0" by auto
  have βpB2: "βp > 2" unfolding βp_def using assms αB2 by auto
  have "ψ A (n+1) = (βp^(n+1) - βm^(n+1))/ α"
    using expr_of_ψ_and_χ[of A α "n+1"] assms α_def2 αB2 βp_def βm_def by fastforce
  hence "ψ A (n+1) = ((βp*βp^n - βp*βm^n) + (βp*βm^n - βm*βm^n))/ α"
    using power_Suc[of βp n] power_Suc[of βm n] by simp
  hence "ψ A (n+1) = (βp*βp^n - βp*βm^n)/ α + (βp*βm^n - βm*βm^n)/ α"
    using add_divide_distrib[of "(βp*βp^n - βp*βm^n)" "(βp*βm^n - βm*βm^n)" α] assms by simp
  hence "ψ A (n+1) = βp*(βp^n-βm^n)/ α + βm^n*(βp-βm)/ α" by (auto simp add: algebra_simps)
  hence "ψ A (n+1) = βp*ψ A n + βm^n*(βp-βm)/ α"
    using βp_def βm_def expr_of_ψ_and_χ[of A α n] α_def2 αB2 assms by fastforce
  hence "ψ A (n+1) = βp*ψ A n + βm^n"
    using βp_def βm_def diff_divide_distrib[of "A+α" "A-α" 2] αB2 apply simp by (simp add: βm_def)
  hence "ψ A (n+1) > βp * ψ A n" using βm_pos by auto
  thus ?thesis using βpB2 lucas_monotone2[of A "0" n] assms mult_right_mono[of 2 βp "ψ A n"] by auto
qed

lemma distinct_residus:
  fixes A::int and n::int and k::int and i::int and j::int
  assumes "A > 2" and "n > 3" and "χ_int A n = 2*k" and "i∈{-n..n}" and "j∈{-n..n}" and "i≠j"
  shows "ψ_int A i mod k ≠ ψ_int A j mod k"
proof -
  have χ_maj: "χ A m > 2 * ψ A m" for m::nat
    using assms χ_is_Bigger_2ψ[of A m] by simp

  have non_null: "l∈{1..n} ⟶ ψ_int A l mod k ≠ 0 ∧ ψ_int A (-l) mod k ≠ 0" for l
  proof
    assume lLen: "l∈{1..n}"
    hence notz: "ψ A (nat l) > 0" using assms lucas_strict_monotonicity[of "A" "nat l-1"] by force
    hence nonzero: "ψ_int A l > 0 ∧ ψ_int A (-l) < 0" unfolding ψ_int_def using lLen by force
    have "ψ A (nat l) ≤ ψ A (nat n)"
      using assms lLen lucas_monotone2[of A "nat l" "nat n - nat l"] by force
    hence "ψ A (nat l) < k"
      using χ_maj[of "nat n"] assms unfolding χ_int_def by auto
    hence "ψ A (nat l) mod k ≠ 0" using notz by simp
    thus "ψ_int A l mod k ≠ 0 ∧ ψ_int A (-l) mod k ≠ 0"
      unfolding ψ_int_def using lLen zmod_zminus1_not_zero by simp
  qed

  have prepart2:"l∈{1..n} ∧ m∈{1..n} ∧ l<m ⟹ ψ_int A l mod k ≠ ψ_int A m mod k" for l m
  proof -
    assume assm: "l∈{1..n} ∧ m∈{1..n} ∧ l<m"
    then have "ψ A (nat l) < ψ A (nat m)"
      using ψ_int_def assms lucas_monotone2[of A "nat l" "nat m - nat l - 1"]
        lucas_strict_monotonicity[of A "nat m -1"] by force
    then have Le: "ψ_int A l < ψ_int A m" using assm ψ_int_def by simp
    have ψlBe0: "ψ_int A l ≥ 0"
      using assms ψ_int_def assm lucas_strict_monotonicity[of A "nat l - 1"] by simp
    have "ψ A (nat m) ≤ ψ A (nat n)"
      using lucas_monotone2[of A "nat m" "nat n - nat m"] assms assm by force
    then have "ψ A (nat m) < k"
      using ‹n>3› ‹χ_int A n = 2*k› χ_maj[of "nat n"] χ_int_def[of A n] by simp
    then have "ψ_int A m < k" using ψ_int_def assm by simp
    then have "0 < ψ_int A m - ψ_int A l ∧ ψ_int A m - ψ_int A l < k" using Le ψlBe0 by auto
    then have "(ψ_int A m - ψ_int A l) mod k ≠ 0" by simp
    then show "ψ_int A l mod k ≠ ψ_int A m mod k" by (metis dvd_imp_mod_0 mod_eq_dvd_iff)
  qed
  then have part2: "l≠m ⟹ l∈{1..n} ∧ m∈{1..n} ⟹ ψ_int A l mod k ≠ ψ_int A m mod k" for l m
  proof (cases "l<m")
    case True
    then show "l∈{1..n} ∧ m∈{1..n} ⟹ ψ_int A l mod k ≠ ψ_int A m mod k"
      using prepart2[of l m] by simp
  next
    case False
    note t=this
    then show "l≠m ⟹ l∈{1..n} ∧ m∈{1..n} ⟹ ψ_int A l mod k ≠ ψ_int A m mod k"
    proof -
      assume "l≠m"
      then have "m<l" using t by simp
      then show "l∈{1..n} ∧ m∈{1..n} ⟹ ψ_int A l mod k ≠ ψ_int A m mod k" using prepart2[of m l]
        by simp
    qed
  qed

  have small_result: "0 < a ∧ a < 2*k ∧ a ≠ k ⟹ ¬ k dvd a" for a
  proof (rule ccontr)
    assume assm: "0 < a ∧ a < 2*k ∧ a ≠ k"
    have k_pos: "k > 0" using χ_maj[of "nat n"] assms χ_int_def[of A n] lucas_strict_monotonicity[of A "nat n-1"]
      by auto
    assume hypoth: "¬ ¬ k dvd a"
    then obtain x where x_def: "k*x = a" by force
    consider (neg) "x ≤ 0" | (1) "x=1" | (pos) "x ≥ 2" by linarith
    then show "False"
    proof (cases)
      case neg
      then show ?thesis using assm by (smt (verit, del_insts) x_def zero_less_mult_pos)
    next
      case 1
      then show ?thesis using assm x_def by simp
    next
      case pos
    then show ?thesis using assm k_pos mult_left_mono[of 2 x k] x_def by auto
    qed
  qed

  have rel_ψ_χ_lin:"2*ψ A x = A*ψ A (x+1) - χ A (x+1)" for x
  proof (induction x rule: ψ_induct)
    case 0
    then show ?case by auto
  next
    case 1
    then show ?case by auto
  next
    case (sucsuc n)
    note t = this
    have "A*ψ A (n+2+1) - χ A (n+2+1) = A*(A*ψ A (n+1+1) - ψ A (n+1)) - (A*χ A (n+1+1) - χ A (n+1))"
      by auto
    hence "A*ψ A (n+2+1) - χ A (n+2+1) = A*(A*ψ A (n+1+1) - χ A (n+1+1)) - (A*ψ A (n+1) - χ A (n+1))"
      by (auto simp add: algebra_simps)
    then show ?case using t by auto
  qed

  have prepart3: "l∈{1..n-1} ⟹ (ψ_int A l + ψ_int A n) mod k ≠ 0 mod k" for l
  proof -
    have ψ_frac: "ψ A m ≤ ψ A (m+1) * 2/5" for m using assms ψ_ineq_opti[of A m] by auto
    assume assm: "l∈{1..n-1}"
    have ψ_pos: "0 < ψ_int A l ∧ 0 < ψ_int A n ∧ 0 < ψ A (nat n)"
      using assms assm ψ_int_def[of A l] ψ_int_def[of A n] lucas_strict_monotonicity[of A "nat l-1"]
        lucas_strict_monotonicity[of A "nat n-1"] by auto
    have lesser_2k: "ψ_int A l + ψ_int A n < 2*k"
      using ψ_int_def[of A l] ψ_int_def[of A n] assm assms lucas_monotone4[of A "nat l" "nat n"]
        χ_maj[of "nat n"] χ_int_def[of A n] apply simp by linarith
    have pos: "ψ_int A l + ψ_int A n > 0" using ψ_pos by auto
    consider (small) "l ≤ n-3" | (n_m2) "l = n-2" | (n_m1) "l = n-1" using assm by force
    then show ?thesis
    proof cases
      case small
      hence ineq1: "ψ_int A l + ψ_int A n ≤ ψ A (nat n - 3) + ψ A (nat n)"
        using assm ψ_int_def[of A l] ψ_int_def[of A n] lucas_monotone4[of A "nat l" "nat n-3"] assms
        by auto
      have nat_eq: "Suc (nat n-3) = nat n-2 ∧ Suc (nat n-2) = nat n-1 ∧ Suc (nat n-1) = nat n"
        using assms by auto
      hence "ψ A (nat n-3) ≤ ψ A (nat n) * 8/125"
        using assms ψ_frac[of "nat n-3"] ψ_frac[of "nat n - 2"] ψ_frac[of "nat n - 1"] by auto
      hence ineq2: "ψ_int A l + ψ_int A n ≤ ψ A (nat n)*(133/125)" using ineq1 by auto
      have ineq3: "133/125 < sqrt (5) / 2"
      proof -
        have obv: "125*sqrt 5 > 0 ∧ (266::int) > 0" by simp
        have obv2: "(133/125 < sqrt (5) / 2) = (266 < 125*sqrt 5)" by auto
        have "266^2 < (125*sqrt 5)^2" by auto
        hence "266 < 125*sqrt 5" using obv by (smt (z3) pos2 power_mono_iff)
        then show ?thesis using obv2 by auto
      qed
      hence "ψ A (nat n)*(133/125) < ψ A (nat n)*(sqrt 5 / 2)"
        using ψ_pos mult_strict_left_mono[of "ψ A (nat n)" "133/125" "sqrt 5 / 2"] by auto
      hence "ψ_int A l + ψ_int A n < (ψ A (nat n) * sqrt 5) / 2" using ineq2 by auto
      hence "ψ_int A l + ψ_int A n < k"
        using assms χ_int_def[of A n] χ_is_Bigger_sqrt5ψ[of A "nat n"]
        by (simp add: mult_of_int_commute)
      then show ?thesis using small_result[of "ψ_int A l + ψ_int A n"] pos lesser_2k by auto
    next
      case n_m2
      have "ψ_int A (n-2) + ψ_int A n ≠ k"
      proof (rule ccontr)
        have dev_nat: "nat (n - 2) = nat n - 2 ∧ nat n = Suc (Suc (nat n - 2))" using assms by auto
        assume hypoth: "¬(ψ_int A (n-2) + ψ_int A n ≠ k)"
        hence "2*(ψ A (nat (n - 2)) + ψ A (nat n)) = χ A (nat n)"
          using assms ψ_int_def[of A "n-2"] ψ_int_def[of A n] χ_int_def[of A n] by auto
        hence "2*(ψ A (nat n - 2) + ψ A (Suc (Suc (nat n - 2)))) = χ A (nat n)"
          using dev_nat by simp
        hence "A*(2*ψ A (Suc (nat n - 2))) = χ A (nat n)" by auto
        hence "A*(A*ψ A (Suc (nat n - 2) + 1) - χ A (Suc (nat n - 2) + 1)) = χ A (nat n)"
          using rel_ψ_χ_lin[of "Suc (nat n - 2)"] by auto
        hence "A*(A*ψ A (nat n) - χ A (nat n)) = χ A (nat n)"
          using assms by (metis Suc_eq_plus1 dev_nat)
        hence "A^2*ψ A (nat n) = (A+1) * χ A (nat n)"
          using power2_eq_square[of A] by (auto simp add: algebra_simps)
        hence "(A^2*ψ A (nat n))^2 = (A+1)^2*((A^2-4)*ψ A (nat n)^2 + 4)"
          using power_mult_distrib[of "A+1" "χ A (nat n)" 2] lucas_pell_part3[of A "nat n"] by auto
        hence "((A+1)^2*(A^2-4)-A^2*A^2)*ψ A (nat n)^2 + 4*(A+1)^2 = 0"
          by (auto simp add: algebra_simps)
        hence "((A^2+2*A+1)*(A^2-4)-A^2*A^2) *ψ A (nat n)^2 + 4*(A+1)^2 = 0"
          using power2_sum[of A 1] apply simp by (smt (verit, best))
        hence "(2*A*A*A-3*A*A-8*A-4)*ψ A (nat n)^2 + 4*(A+1)^2 = 0"
          using power2_eq_square[of A] by (auto simp add: algebra_simps)
        hence equation: "((2*A+1)*(A+1)*(A-3)-1)*ψ A (nat n)^2 + 4*(A+1)^2 = 0"
          by (auto simp add: algebra_simps)
        have "4*(A+1)^2 ≥ 64"
          using assms power2_eq_square[of "A+1"] mult_mono[of 4 "A+1" 4 "A+1"] by auto
        hence "((2*A+1)*(A+1)*(A-3)-1)*ψ A (nat n)^2 ≤ -64" using equation by auto
        hence "((2*A+1)*(A+1)*(A-3)-1) < 0"
          by (smt (verit, ccfv_SIG) ψ_pos assms(1) int_distrib(2) pos_zmult_eq_1_iff zero_less_power zmult_zless_mono2)
        hence ineq2: "(2*A+1)*(A+1)*(A-3) ≤ 0" by auto
        have "(2*A+1)*(A+1) > 0" using assms by auto
        hence "A=3" using ineq2 assms by (smt (verit) mult_pos_pos)
        hence "8^2 = ψ 3 (nat n)^2 " using equation by auto
        hence eq: "8 = ψ 3 (nat n)" using lucas_strict_monotonicity[of 3 "nat n-1"] assms apply simp
          by (smt (verit, ccfv_SIG) ‹8⇧2 = (ψ 3 (nat n))⇧2› power2_eq_imp_eq)
        have "ψ 3 3 = ψ 3 (Suc (Suc (Suc 0)))" using numeral_3_eq_3 by presburger
        hence eq2: "ψ 3 3 = ψ 3 (nat n)" using eq by auto
        hence "ψ 3 (Suc 3) > ψ 3 (nat n) ∧ nat n ≥ Suc 3" using lucas_strict_monotonicity[of 3 3] assms by auto
        then show "False" using lucas_monotone4[of 3 "Suc 3" "nat n"] assms by auto
      qed
      hence "ψ_int A l + ψ_int A n ≠ k" using n_m2 by auto
     then show ?thesis using pos lesser_2k small_result[of "ψ_int A l + ψ_int A n"] by auto
    next
      case n_m1
      have "ψ_int A (n-1) + ψ_int A n ≠ k"
      proof (rule ccontr)
        have dev_nat: "nat (n-1) = nat n - 1 ∧ nat n - 1 +1 = nat n" using assms by auto
        assume hypoth: "¬(ψ_int A (n-1) + ψ_int A n ≠ k)"
        hence "2*ψ A (nat n - 1) + 2*ψ A (nat n) = χ A (nat n)"
          using assms ψ_int_def[of A "n-1"] ψ_int_def[of A n] χ_int_def[of A n] dev_nat by auto
        hence "A*ψ A (nat n) - χ A (nat n) + 2*ψ A (nat n) = χ A (nat n)"
          using rel_ψ_χ_lin[of "nat n - 1"] dev_nat by auto
        hence "(A+2)*ψ A (nat n) = 2*χ A (nat n)" by (auto simp add: algebra_simps)
        hence "(A+2)^2*ψ A (nat n)^2 = 4*((A^2-4)*ψ A (nat n)^2 +4)"
          using lucas_pell_part3[of A "nat n"] power_mult_distrib[of "A+2" "ψ A (nat n)" 2]
          by (auto simp add: algebra_simps)
        hence "(4*(A^2-4) - (A+2)^2)*ψ A (nat n)^2 + 16 = 0" by (auto simp add: algebra_simps)
        hence "(3*A*A-20 - 4*A)*ψ A (nat n)^2 +16 = 0"
          using power2_eq_square[of A] power2_sum[of A 2] by (auto simp add: algebra_simps)
        hence equation: "(3*A-10)*(A+2)*ψ A (nat n)^2 + 16 = 0" by (auto simp add: algebra_simps)
        have "(A+2)*ψ A (nat n)^2 > 0" using ψ_pos assms by auto
        hence "3*A-10 < 0"
          using equation by (smt (verit, ccfv_SIG) int_distrib(4) zmult_zless_mono2)
        hence "A=3" using assms by auto
        hence "5*ψ 3 (nat n)^2 = 16" using equation by auto
        hence "0 mod 5 = (16::int) mod 5" by presburger
      then show "False" by simp
    qed
    hence "ψ_int A l + ψ_int A n ≠ k" using n_m1 by auto
     then show ?thesis using pos lesser_2k small_result[of "ψ_int A l + ψ_int A n"] by auto
   qed
 qed

  have part3: "l∈{1..n} ∧ m∈{-n..-1} ⟹ ψ_int A l mod k ≠ ψ_int A m mod k" for l m
  proof -
    assume assm: "l∈{1..n} ∧ m∈{-n..-1}"
    define h where "h = -m"
    consider (lesser_n) "l<n ∧ h<n" | (less_eq) "l<n ∧ h=n" | (eq_less) "l=n ∧ h<n"
            | (eq_n) "l=n ∧ h=n"
      using assm h_def apply simp by linarith
    thus ?thesis
    proof cases
      case lesser_n
      have lh_pos: "l > 0 ∧ h > 0" using assm h_def by auto
      have "ψ_int A l - ψ_int A m = ψ_int A l + ψ_int A h" using ψ_int_odd h_def by simp
      hence eq1: "ψ_int A l - ψ_int A m = ψ A (nat l) + ψ A (nat h)" using lh_pos ψ_int_def by auto
      hence diff_pos: "ψ_int A l - ψ_int A m > 0"
        using assms lucas_strict_monotonicity[of A "nat l - 1"] lucas_strict_monotonicity[of A "nat h - 1"] lh_pos by auto
      have "nat l ≤ nat n - 1 ∧ nat h ≤ nat n - 1" using lesser_n h_def by auto 
      have obv: "nat n - 1 + 1 = nat n ∧ nat n - 1 > 2" using assms by auto
      have "ψ A (nat l) + ψ A (nat h) ≤2*ψ A (nat n-1)"
        using lesser_n lucas_monotone4[of A "nat l" "nat n-1"] lucas_monotone4[of A "nat h" "nat n-1"]
          assms by linarith
      hence "ψ_int A l - ψ_int A m < ψ A (nat n)" using eq1 ψ_doubles[of A "nat n-1"] assms obv
        by auto
      hence "ψ_int A l - ψ_int A m < k" using χ_maj[of "nat n"] χ_int_def[of A n] assms
        by simp
      hence "(ψ_int A l - ψ_int A m) mod k ≠ 0 mod k" using diff_pos by auto
      then show ?thesis using mod_diff_cong by fastforce
    next
      case less_eq
      hence "(ψ_int A h + ψ_int A l) mod k ≠ 0 mod k"
        using prepart3[of l] assm by (simp add: add.commute)
      hence "(ψ_int A l - ψ_int A m) mod k ≠ 0 mod k" using h_def ψ_int_odd by auto 
      then show ?thesis using mod_diff_cong by fastforce
    next
      case eq_less
      hence "(ψ_int A h + ψ_int A l) mod k ≠ 0 mod k"
        using prepart3[of h] assm h_def by (simp add: add.commute)
      hence "(ψ_int A l - ψ_int A m) mod k ≠ 0 mod k" using h_def ψ_int_odd by auto
      then show ?thesis using mod_diff_cong by fastforce
    next
      case eq_n
      have ψB2: "ψ A (nat n) > 2" using lucas_monotone3[of A "nat n"] assms by auto
      have fund: "(20-A^2)*(ψ A (nat n))^2 ≠ 4"
      proof (cases "20-A^2 = 0")
        case True
        then show ?thesis by simp
      next
        case False
        have "abs ((20 - A^2)*(ψ A (nat n))^2) = abs (20 - A^2) * (ψ A (nat n) * ψ A (nat n))"
          using abs_mult[of "20-A^2" "ψ A (nat n)^2"] ψB2 power2_eq_square[of "ψ A (nat n)"]
            abs_mult[of "ψ A (nat n)" "ψ A (nat n)"] by auto
        hence "abs ((20 - A^2)*(ψ A (nat n))^2) ≥ ψ A (nat n) * ψ A (nat n)" 
          using False mult_right_mono[of 1 "abs (20 - A^2)" "ψ A (nat n) * ψ A (nat n)"] by auto
        hence "abs ((20 - A^2)*(ψ A (nat n))^2) > 4"
          using ψB2 mult_strict_mono[of 2 "ψ A (nat n)" 2 "ψ A (nat n)"]
          by (auto simp add: mult_strict_mono)
        then show ?thesis by auto
      qed
      have "(20-A^2)*(ψ A (nat n))^2 = 4^2*(ψ A (nat n))^2 - (A^2-4)*(ψ A (nat n))^2"
        by (auto simp add: algebra_simps)
      hence "(20-A^2)*(ψ A (nat n))^2 = (4*(ψ A (nat n)))^2 - χ A (nat n)^2 + 4"
        using lucas_pell_part3[of A "nat n"] by (auto simp add: algebra_simps)
      hence "(4*(ψ A (nat n)))^2 - χ A (nat n)^2 ≠ 0" using fund by auto
      hence "4*ψ A (nat n) ≠ χ A (nat n)" by algebra
      hence not_k: "ψ_int A l + ψ_int A h ≠ k" using assms eq_n ψ_int_def[of A n]
        using χ_int_def add_cancel_right_right left_minus_one_mult_self
          mult.commute mult.left_commute power_add by fastforce
      have pos: "ψ_int A l + ψ_int A h > 0" using eq_n ψ_int_def[of A n] ψB2 by auto
      have lesser_χ: "ψ_int A l + ψ_int A h < 2*k"
        using assms eq_n χ_maj[of "nat n"] ψ_int_def[of A n] χ_int_def[of A n] by auto
      have not_dvd: "¬ (k dvd (ψ_int A l + ψ_int A h))"
        using small_result[of "ψ_int A l + ψ_int A h"] pos not_k lesser_χ by auto
      hence "(ψ_int A l - ψ_int A m) mod k ≠ 0 mod k" using ψ_int_odd[of A m] h_def by auto
      then show ?thesis using mod_diff_cong by fastforce
    qed
  qed

  consider (null_pos) "i=0 ∧ j>0" | (null_neg) "i=0 ∧ j<0" |
          (pos_null) "i>0 ∧ j=0" | (pos_pos) "i>0 ∧ j>0 ∧ i≠j" | (pos_neg) "i>0 ∧ j<0" |
          (neg_null) "i<0 ∧ j=0" | (neg_pos) "i<0 ∧ j>0" | (neg_neg) "i<0 ∧ j<0 ∧ i≠j"
    using ‹j ∈ {- n..n}› ‹i ∈ {- n..n}› by (metis assms(6) linorder_neqE_linordered_idom)
  then show ?thesis 
  proof cases
    case null_pos
    then show ?thesis using  ψ_int_def non_null[of j] ‹j ∈ {- n..n}› by force
    next
      case null_neg
      then show ?thesis using ψ_int_def non_null[of "-j"] ‹j ∈ {- n..n}› by force
    next
      case pos_null
      then show ?thesis using ψ_int_def non_null[of "i"] ‹i ∈ {- n..n}› by force
    next
      case pos_pos
      then show ?thesis using ψ_int_def part2[of "i" "j"] ‹i ∈ {- n..n}› ‹j ∈ {- n..n}› by force
    next
      case pos_neg
      then show ?thesis using part3[of i j] assms by auto
    next
      case neg_null
      then show ?thesis using ψ_int_def non_null[of "-i"] ‹i ∈ {- n..n}› by force
    next
      case neg_pos
      then show ?thesis using part3[of j i] assms by auto
    next
      case neg_neg
      then show ?thesis using ψ_int_def part2[of "-i" "-j"] ‹i ∈ {- n..n}› ‹j ∈ {- n..n}›
        apply simp by (metis equation_minus_iff mod_minus_cong)
  qed
qed


lemma case_lesser_than_4n:
  fixes A::int and n::int and s::int  and t::int and k::int
  assumes "A > 2" and "n > 3" and "χ_int A n = 2*k" and "0≤s ∧ s<4*n ∧ 0≤t ∧ t<4*n"
  shows "(ψ_int A s mod k = ψ_int A t mod k)
      ⟹ (s mod (4*n) = t mod (4*n) ∨ (s+t) mod (4*n) = (2*n) mod (4*n))"
proof -
  assume ψ_eq: "ψ_int A s mod k = ψ_int A t mod k"
  consider (11) "0≤ s ∧ s≤n ∧ 0≤t   ∧ t≤n  " | (21) "n≤s ∧ s≤3*n ∧ 0≤t   ∧ t≤n  " | (41) "3*n≤s ∧ s≤4*n ∧ 0≤t   ∧ t≤n  " |
           (12) "0≤ s ∧ s≤n ∧ n≤t   ∧ t≤3*n" | (22) "n≤s ∧ s≤3*n ∧ n≤t   ∧ t≤3*n" | (42) "3*n≤s ∧ s≤4*n ∧ n≤t ∧ t≤3*n" |
           (14) "0≤ s ∧ s≤n ∧ 3*n≤t ∧ t≤4*n" | (24) "n≤s ∧ s≤3*n ∧ 3*n≤t ∧ t≤4*n" | (44) "3*n≤s ∧ s≤4*n ∧ 3*n≤t ∧ t≤4*n"
    using assms by (smt (verit) "11")
  thus ?thesis
  proof (cases)
    case 11
    have "s=t" using distinct_residus[of A n k s t] assms ψ_eq "11" by auto
then show ?thesis by simp
next
  case 21
  have ineq: "-n ≤ 2*n-s ∧ 2*n-s ≤ n" using "21" by auto
  have "ψ_int A (2*n-s) mod k = ψ_int A t mod k"
    using assms ψ_eq technical_lemma2[of n A k "-s"] ψ_int_odd[of A "-s"]
    by (smt (z3) sun_lemma10_rec)
  hence "t = 2*n-s" using distinct_residus[of A n k "2*n-s" t] "21" ineq assms by auto
  then show ?thesis by simp
next
  case 41
  have ineq: "-n ≤ -4*n+s ∧ -4*n+s ≤n" using "41" by auto
  have "ψ_int A (-4*n+s) mod k = ψ_int A t mod k"
    using technical_lemma2_part2[of n A k "-1" s] ψ_eq assms by auto
  hence "t = -4*n+s" using distinct_residus[of A n k "-4*n+s" t] "41" ineq assms by auto
  then show ?thesis by simp
next
  case 12
  have ineq: "-n ≤ 2*n-t ∧ 2*n-t ≤ n" using "12" by auto
  have "ψ_int A (2*n-t) mod k = ψ_int A s mod k"
    using assms ψ_eq technical_lemma2[of n A k "-t"] ψ_int_odd[of A "-t"]
    by (smt (z3) sun_lemma10_rec)
  hence "s = 2*n-t" using distinct_residus[of A n k "2*n-t" s] "12" ineq assms by auto
  then show ?thesis by simp
next
  case 22
  have ineq: "-n ≤ 2*n-s ∧ 2*n-s ≤ n ∧ -n ≤ 2*n-t ∧ 2*n-t ≤ n" using "22" by auto
  have "ψ_int A (2*n-s) mod k = ψ_int A (2*n-t) mod k"
    using assms ψ_eq technical_lemma2[of n A k "-t"] technical_lemma2[of n A k "-s"]
      ψ_int_odd[of A "-s"] ψ_int_odd[of A "-s"] by (smt (z3) sun_lemma10_rec)
  hence "2*n-s = 2*n-t" using distinct_residus[of A n k "2*n-t" "2*n-s"] ineq assms by auto
  then show ?thesis by simp
next
  case 42
  have ineq: "-n ≤ s-4*n ∧ s-4*n ≤ n ∧ -n ≤ 2*n-t ∧ 2*n-t ≤ n" using "42" by auto
  have "ψ_int A (s-4*n) mod k = ψ_int A (2*n-t) mod k"
    using assms ψ_eq technical_lemma2[of n A k "-t"] technical_lemma2_part2[of n A k "-1" s]
      ψ_int_odd[of A "-t"] by (smt (z3) sun_lemma10_rec)
  hence "s-4*n = 2*n - t" using distinct_residus[of A n k "s-4*n" "2*n-t"] ineq assms by auto
  then show ?thesis by simp
next
  case 14
  have ineq: "-n ≤ -4*n+t ∧ -4*n+t ≤n" using "14" by auto
  have "ψ_int A (-4*n+t) mod k = ψ_int A s mod k"
    using technical_lemma2_part2[of n A k "-1" t] ψ_eq assms by auto
  hence "s = -4*n+t" using distinct_residus[of A n k "-4*n+t" s] "14" ineq assms by auto
  then show ?thesis by simp
next
  case 24
  have ineq: "-n ≤ t-4*n ∧ t-4*n ≤ n ∧ -n ≤ 2*n-s ∧ 2*n-s ≤ n" using "24" by auto
  have "ψ_int A (t-4*n) mod k = ψ_int A (2*n-s) mod k"
    using assms ψ_eq technical_lemma2[of n A k "-s"] technical_lemma2_part2[of n A k "-1" t]
      ψ_int_odd[of A "-s"] by (smt (z3) sun_lemma10_rec)
  hence "t-4*n = 2*n - s" using distinct_residus[of A n k "t-4*n" "2*n-s"] ineq assms by auto
  then show ?thesis by simp
next
  case 44
  have ineq: "-n ≤ s-4*n ∧ s-4*n ≤ n ∧ -n ≤ t-4*n ∧ t-4*n ≤ n" using "44" by auto
  have "ψ_int A (s-4*n) mod k = ψ_int A (t-4*n) mod k"
    using assms ψ_eq technical_lemma2_part2[of n A k "-1" s] technical_lemma2_part2[of n A k "-1" t]
    by (smt (z3) sun_lemma10_rec)
  then show ?thesis using distinct_residus[of A n k "t-4*n" "s-4*n"] ineq assms by auto
qed
qed

lemma mod_pos:
  fixes k::int and n::int
  assumes "n > 0"
  shows "0 ≤ k mod n ∧ k mod n < n"
  by (simp add: assms)

lemma lesser_4n_to_all:
  fixes A::int and n::int and s::int and t::int and k::int
  assumes "A > 2" and "n > 3" and "χ_int A n = 2*k"
  shows "(ψ_int A s mod k = ψ_int A t mod k)
      ⟹ (s mod (4*n) = t mod (4*n) ∨ (s+t) mod (4*n) = (2*n) mod (4*n))"
proof -
  assume hyp_true: "ψ_int A s mod k = ψ_int A t mod k"
  have dvd_mod: "a dvd b ⟹ l mod b = m mod b ⟹ l mod a = m mod a" for a::int and b and l and m
    by (metis mod_mod_cancel)
  define s0 where "s0 = s mod (4*n)"
  define t0 where "t0 = t mod (4*n)"
  have hyp_s: "s mod (4*n) = s0 mod (4*n) ∧ 0 ≤ s0 ∧ s0 < 4*n" unfolding s0_def using assms by auto
  have hyp_t: "t mod (4*n) = t0 mod (4*n) ∧ 0 ≤ t0 ∧ t0 < 4*n" unfolding t0_def using assms by auto
  have "(s+t) mod (4*n) = (s0+t0) mod (4*n)" using hyp_s hyp_t mod_add_cong[of s "4*n" s0 t t0]
    by auto
  hence impl: "(s0 mod (4*n) = t0 mod (4*n) ∨ (s0+t0) mod (4*n) = (2*n) mod (4*n))
      ⟹ (s mod (4*n) = t mod (4*n) ∨ (s+t) mod (4*n) = (2*n) mod (4*n))"
    using hyp_s hyp_t by auto
  obtain qs where qs_def: "s = 4*n*qs + s0" using s0_def by (metis mult_div_mod_eq)
  obtain qt where qt_def: "t = 4*n*qt + t0" using t0_def by (metis mult_div_mod_eq)
  have "ψ_int A s mod k = ψ_int A s0 mod k ∧ ψ_int A t mod k = ψ_int A t0 mod k"
    using technical_lemma2_part2[of n A k qs s0] qs_def assms 
    technical_lemma2_part2[of n A k qt t0] qt_def by auto
  hence "ψ_int A s0 mod k = ψ_int A t0 mod k" using hyp_true by auto
  then have "s0 mod (4*n) = t0 mod (4*n) ∨ (s0+t0) mod (4*n) = (2*n) mod (4*n)"
    using case_lesser_than_4n[of A n k s0 t0] assms hyp_s hyp_t by auto
  thus "s mod (4*n) = t mod (4*n) ∨ (s+t) mod (4*n) = (2*n) mod (4*n)" using impl by auto
qed

lemma sun_lemma10_dir:
  fixes A::int and n::int and s::int and t::int and k::int
  assumes "A > 2" and "n > 3" and "χ_int A n = 2*k"
  shows "(ψ_int A s mod k = ψ_int A t mod k)
      ⟹ (s mod (4*n) = t mod (4*n) ∨ (s+t) mod (4*n) = (2*n) mod (4*n))"
  using assms lesser_4n_to_all[of A n k s t] by simp

lemma (in bridge_variables) sun_lemma24:
  fixes A::int and B::int and C::int and x::int and y::int
  assumes "abs A ≥ 2"
  shows "is_square (D_f A C * F_ACx A C x * I_ABCxy A B C x y) = (is_square (D_f A C)
      ∧ is_square (F_ACx A C x) ∧ is_square (I_ABCxy A B C x y))"
proof -
  have converse: "(is_square (D_f A C) ∧ is_square (F_ACx A C x) ∧ is_square (I_ABCxy A B C x y))
      ⟹ is_square (D_f A C * F_ACx A C x * I_ABCxy A B C x y)"
  proof -
    assume "(is_square (D_f A C) ∧ is_square (F_ACx A C x) ∧ is_square (I_ABCxy A B C x y))"
    then obtain d f i where "D_f A C = d^2 ∧ F_ACx A C x = f^2 ∧ I_ABCxy A B C x y = i^2"
      by (auto simp add: is_square_def)
    hence "D_f A C * F_ACx A C x * I_ABCxy A B C x y = (d*f*i)^2" by (auto simp add: algebra_simps)
    thus ?thesis using is_square_def by auto
  qed
  have direct: "is_square (D_f A C * F_ACx A C x * I_ABCxy A B C x y)
      ⟹ ((is_square (D_f A C) ∧ is_square (F_ACx A C x) ∧ is_square (I_ABCxy A B C x y)))"
  proof -
    assume hyp: "is_square (D_f A C * F_ACx A C x * I_ABCxy A B C x y)"
    have square_decomp: "is_square (a*b) ∧ coprime a b ∧ a ≥ 0 ∧ b ≥ 0 ⟹ is_square a ∧ is_square b"
      for a b :: int
    proof -
      assume hypo: "is_square (a*b) ∧ coprime a b ∧ a ≥ 0 ∧ b ≥ 0"
      then obtain k where k_def: "a*b = k^2" using is_square_def by auto
      define c where "c = gcd a k"
      define d where "d = gcd b k"
      have eq1: "c*c dvd a*b ∧ d*d dvd a*b" using c_def d_def k_def power2_eq_square[of k]
        by (auto simp add: mult_dvd_mono)
      have "coprime c b ∧ coprime d a" using c_def d_def hypo coprime_divisors[of c a b b]
          coprime_divisors[of d b a a] by (simp add: coprime_commute)
      hence cop: "coprime (c*c) b ∧ coprime (d*d) a" by auto
      hence eq2: "c*c dvd a ∧ d*d dvd b" using eq1 by (meson coprime_dvd_mult_left_iff euclids_lemma)
      have "k dvd a*b" using k_def by auto
      hence "k dvd c*d" using c_def d_def apply simp
        by (metis (no_types, lifting) division_decomp dvd_triv_left dvd_triv_right gcd_greatest_iff mult_dvd_mono)
      hence "a*b dvd (c*d*c*d)" using k_def power2_eq_square[of k] by auto
      hence "a dvd (d*d)*(c*c) ∧ b dvd (c*c)*(d*d)" by (metis dvd_mult_right mult.assoc mult.commute)
      hence "a dvd (c*c) ∧ b dvd (d*d)"
        using cop euclids_lemma[of a "d*d" "c*c"] coprime_commute[of a "d*d"]
          euclids_lemma[of b "c*c" "d*d"] coprime_commute[of b "c*c"] by auto
      hence "a=c*c ∧ b=d*d"
        using eq2 hypo zdvd_antisym_nonneg zero_le_square
        by simp
      thus ?thesis using is_square_def[of a] is_square_def[of b] power2_eq_square[of c]
          power2_eq_square[of d] by metis
    qed
    have copFD: "coprime (F_ACx A C x) (D_f A C)"
    proof -
      have "F_ACx A C x mod (D_f A C) = (4*(A^2-4)*(C^2*D_f A C*x)^2+1) mod (D_f A C)"
        unfolding F_ACx_def F_f_def E_ACx_def E_f_def by simp
      hence "F_ACx A C x mod (D_f A C) = (4*(A^2-4)*(C^2*x)^2*D_f A C*D_f A C+1) mod (D_f A C)"
        using power_mult_distrib[of "C^2*x" "D_f A C" 2] power2_eq_square[of "D_f A C"]
        by (auto simp add: algebra_simps)
      hence "F_ACx A C x mod (D_f A C) = 1 mod (D_f A C)" by auto
      thus ?thesis by (metis coprimeI coprime_mod_left_iff mod_by_0)
    qed
    have copID: "coprime (I_ABCxy A B C x y) (D_f A C)"
    proof -
      have "G_ACx A C x mod (D_f A C)
      = (1 + (C*F_ACx A C x)* D_f A C - 2*(A+2)*(A-2)^2*(C^2*D_f A C*x)^2) mod (D_f A C)" 
        unfolding G_ACx_def G_f_def E_ACx_def E_f_def by (auto simp add: algebra_simps)
      hence "G_ACx A C x mod (D_f A C)
      = (1 + (C*F_ACx A C x)* D_f A C - 2*(A+2)*(A-2)^2*(C^2*x)^2*D_f A C* D_f A C) mod (D_f A C)"
        using power2_eq_square[of "D_f A C"] power_mult_distrib[of "D_f A C"]
        by (auto simp add: algebra_simps)
      hence "G_ACx A C x mod (D_f A C) = 1 mod (D_f A C)" by (smt (z3) mod_mult_self3)
      hence "(G_ACx A C x^2 - 1) mod (D_f A C) = 0 mod (D_f A C)"
        by (metis cancel_comm_monoid_add_class.diff_cancel mod_diff_left_eq power_mod power_one)
      hence "((G_ACx A C x^2 - 1)*H_ABCxy A B C x y) mod (D_f A C) = 0 mod (D_f A C)" by auto
      hence "I_ABCxy A B C x y mod (D_f A C) = 1 mod (D_f A C)" unfolding I_ABCxy_def I_f_def
        using mod_add_cong[of "(G_ACx A C x^2 - 1)*H_ABCxy A B C x y" "D_f A C" 0 1 1] apply simp
        by (metis (no_types) ‹((G_ACx A C x)⇧2 - 1) mod D_f A C = 0 mod D_f A C› mod_add_left_eq mod_mult_left_eq mod_mult_self2_is_0 mod_mult_self4 mult_numeral_1)
      thus ?thesis by (metis coprimeI coprime_mod_left_iff mod_by_0)
    qed
    have "2*G_ACx A C x mod (F_ACx A C x)
      = (2*C*D_f A C * F_ACx A C x + (2-4*(A+2)*(A-2)^2*E_ACx A C x^2)) mod (F_ACx A C x)"
      unfolding G_ACx_def G_f_def by (auto simp add: algebra_simps)
    hence "2*G_ACx A C x mod (F_ACx A C x) = (2-4*(A+2)*(A-2)^2*E_ACx A C x^2) mod (F_ACx A C x)"
      by auto
    hence "2*G_ACx A C x mod (F_ACx A C x) = (2-4*(A^2-4)*E_ACx A C x^2 * (A-2)) mod (F_ACx A C x)"
      by (auto simp add: algebra_simps power2_eq_square)
    hence "2*G_ACx A C x mod (F_ACx A C x) = (2-(F_ACx A C x-1) * (A-2)) mod (F_ACx A C x)"
      unfolding F_ACx_def F_f_def by auto
    hence "2*G_ACx A C x mod (F_ACx A C x) = (A - (A-2)*F_ACx A C x) mod (F_ACx A C x)"
      by (auto simp add: algebra_simps)
    hence A_eq_2G_modF:  "2*G_ACx A C x mod (F_ACx A C x) = A mod (F_ACx A C x)"
      by (metis add.commute diff_add_cancel mod_mult_self3)
    have copIF: "coprime (I_ABCxy A B C x y) (F_ACx A C x)"
    proof -
      have "H_ABCxy A B C x y mod (F_ACx A C x) = C mod (F_ACx A C x)"
        unfolding H_ABCxy_def H_f_def by auto
      hence "H_ABCxy A B C x y^2 mod (F_ACx A C x) = C^2 mod (F_ACx A C x)" by (metis power_mod)
      hence H_eqC: "((A^2-4)*H_ABCxy A B C x y^2 +4) mod (F_ACx A C x) = D_f A C mod (F_ACx A C x)"
        using mod_mult_cong[of "A^2-4" "F_ACx A C x" "A^2-4" "H_ABCxy A B C x y^2" "C^2"]
        unfolding D_f_def by (metis (no_types) add.commute mod_add_right_eq)
      have "((2*G_ACx A C x)*(2*G_ACx A C x)-4) mod (F_ACx A C x) = (A*A-4) mod (F_ACx A C x)"
        using A_eq_2G_modF by (metis (no_types) mod_diff_left_eq mod_mult_left_eq mod_mult_right_eq)
      hence A_eq2G: "(((2*G_ACx A C x)*(2*G_ACx A C x)-4)*H_ABCxy A B C x y^2 +4) mod (F_ACx A C x)
          = ((A*A-4)*H_ABCxy A B C x y^2 +4) mod (F_ACx A C x)"
        using mod_mult_cong[of "((2*G_ACx A C x)*(2*G_ACx A C x)-4)" "F_ACx A C x" "A*A-4"
            "H_ABCxy A B C x y^2" "H_ABCxy A B C x y^2"]
        by (smt (verit, ccfv_SIG) add.commute mod_add_right_eq)
      have "4*I_ABCxy A B C x y mod (F_ACx A C x)
          = 4*((G_ACx A C x^2-1)*H_ABCxy A B C x y^2 +1) mod (F_ACx A C x)"
        unfolding I_ABCxy_def I_f_def by auto
      hence "4*I_ABCxy A B C x y mod (F_ACx A C x)
          = (((2*G_ACx A C x)^2-4)*H_ABCxy A B C x y^2 +4) mod (F_ACx A C x)"
        using power_mult_distrib[of 2 "G_ACx A C x" 2] by (auto simp add: algebra_simps)
      hence "4*I_ABCxy A B C x y mod (F_ACx A C x)
          = (((2*G_ACx A C x)*(2*G_ACx A C x)-4)*H_ABCxy A B C x y^2 +4) mod (F_ACx A C x)"
        by (auto simp add: power2_eq_square)
      hence "4*I_ABCxy A B C x y mod (F_ACx A C x) = ((A*A-4)*H_ABCxy A B C x y^2 +4) mod (F_ACx A C x)"
        using A_eq2G by auto
      hence "4*I_ABCxy A B C x y mod (F_ACx A C x) = ((A^2-4)*H_ABCxy A B C x y^2 +4) mod (F_ACx A C x)"
        using power2_eq_square[of A] by auto
      hence "4*I_ABCxy A B C x y mod (F_ACx A C x) = D_f A C mod (F_ACx A C x)" using H_eqC by auto
      hence "gcd (4*I_ABCxy A B C x y) (F_ACx A C x) = gcd (D_f A C) (F_ACx A C x)"
        by (metis gcd_red_int)
      hence "coprime (4*I_ABCxy A B C x y) (F_ACx A C x)"
        using copFD by (metis coprime_iff_gcd_eq_1 gcd.commute)
      then show ?thesis by simp
    qed
    have A_pos: "A^2-4 ≥ 0"
      using assms power2_eq_square[of "abs A"] mult_mono[of 2 "abs A" 2 "abs A"] by auto
    hence D_pos: "D_f A C ≥ 1" unfolding D_f_def by auto
    have F_pos: "F_ACx A C x ≥ 1" unfolding F_ACx_def F_f_def using A_pos by auto
    obtain k where "D_f A C * F_ACx A C x * I_ABCxy A B C x y = k^2" using hyp is_square_def by auto
    hence I_pos: "I_ABCxy A B C x y ≥ 0" using D_pos F_pos
      by (smt (verit, ccfv_SIG) mult_pos_neg mult_pos_pos zero_le_power2)
    have copDF_I: "coprime (D_f A C * F_ACx A C x) (I_ABCxy A B C x y)"
      using copID copIF coprime_commute by auto
    hence "is_square (I_ABCxy A B C x y) ∧ is_square (D_f A C * F_ACx A C x)"
      using I_pos D_pos F_pos square_decomp[of "D_f A C * F_ACx A C x" "I_ABCxy A B C x y"] hyp
      by auto
    then show ?thesis
      using square_decomp[of "D_f A C" "F_ACx A C x"]  D_pos F_pos copFD coprime_commute by auto
  qed
  show ?thesis using direct converse by argo
qed

end