Theory FourSquares
section ‹Lagrange's four-square theorem›
theory FourSquares
imports "HOL-Number_Theory.Number_Theory"
begin
context
fixes sum4sq_nat :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat"
defines "sum4sq_nat a b c d ≡ a^2+b^2+c^2+d^2"
fixes is_sum4sq_nat :: "nat ⇒ bool"
defines "is_sum4sq_nat n ≡ (∃ a b c d. n = sum4sq_nat a b c d)"
begin
private lemma best_division_abs: "(n::int) > 0 ⟹ ∃ k. 2 * ¦a - k*n¦ ≤ n"
proof -
assume a: "n > 0"
define k where "k = a div n"
have h: "a - k * n = a mod n" by (simp add: div_mult_mod_eq algebra_simps k_def)
thus ?thesis
proof (cases "2 * (a mod n) ≤ n")
case True
hence "2 * ¦a - k*n¦ ≤ n" using h pos_mod_sign a by auto
thus ?thesis by blast
next
case False
hence "2 * (n - a mod n) ≤ n" by auto
have "a - (k+1)*n = a mod n - n" using h by (simp add: algebra_simps)
hence "2 * ¦a - (k+1)*n¦ ≤ n" using h pos_mod_bound[of n a] a False by fastforce
thus ?thesis by blast
qed
qed
text ‹Shows that all nonnegative integers can be written as the sum of four squares. The proof consists of the following steps:
\begin{itemize}\item For every prime $p=2n+1$ the two sets of residue classes $$\{x^2 \bmod p\mid 0\le x\le n\} ~{\rm and}~ \{-1-y^2 \bmod p \mid 0 \le y \le n\}$$ both contain $n+1$ different elements and therefore they must have at least one element in common.
\item Hence there exist $x,y$ such that $x^2+y^2+1^2+0^2$ is a multiple of $p$.
\item The next step is to show, by an infinite descent, that $p$ itself can be written as the sum of four squares.
\item Finally, using the multiplicity of this form, the same holds for all positive numbers.
\end{itemize}›
private definition
sum4sq_int :: "int × int × int × int ⇒ int" where
"sum4sq_int = (λ(a,b,c,d). a^2+b^2+c^2+d^2)"
private definition
is_sum4sq_int :: "int ⇒ bool" where
"is_sum4sq_int n ⟷ (∃ a b c d. n = sum4sq_int(a,b,c,d))"
private lemma mult_sum4sq_int: "sum4sq_int(a,b,c,d) * sum4sq_int(p,q,r,s) =
sum4sq_int(a*p+b*q+c*r+d*s, a*q-b*p-c*s+d*r,
a*r+b*s-c*p-d*q, a*s-b*r+c*q-d*p)"
by (unfold sum4sq_int_def, simp add: eval_nat_numeral field_simps)
private lemma sum4sq_int_nat_eq: "sum4sq_nat a b c d = sum4sq_int (a, b, c, d)"
unfolding sum4sq_nat_def sum4sq_int_def by simp
private lemma is_sum4sq_int_nat_eq: "is_sum4sq_nat n = is_sum4sq_int (int n)"
unfolding is_sum4sq_nat_def is_sum4sq_int_def
proof
assume "∃a b c d. n = sum4sq_nat a b c d"
thus "∃a b c d. int n = sum4sq_int (a, b, c, d)" using sum4sq_int_nat_eq by force
next
assume "∃a b c d. int n = sum4sq_int (a, b, c, d)"
then obtain a b c d where "int n = sum4sq_int (a, b, c, d)" by blast
hence "int n = sum4sq_int (int (nat ¦a¦), int (nat ¦b¦), int (nat ¦c¦), int (nat ¦d¦))"
unfolding sum4sq_int_def by simp
hence "int n = int (sum4sq_nat (nat ¦a¦) (nat ¦b¦) (nat ¦c¦) (nat ¦d¦))"
using sum4sq_int_nat_eq by presburger
thus "∃a b c d. n = sum4sq_nat a b c d" by auto
qed
private lemma is_mult_sum4sq_int: "is_sum4sq_int x ⟹ is_sum4sq_int y ⟹ is_sum4sq_int (x*y)"
by (unfold is_sum4sq_int_def, auto simp only: mult_sum4sq_int, blast)
private lemma is_mult_sum4sq_nat: "is_sum4sq_nat x ⟹ is_sum4sq_nat y ⟹ is_sum4sq_nat (x*y)"
using is_mult_sum4sq_int is_sum4sq_int_nat_eq by simp
private lemma mult_oddprime_is_sum4sq: "⟦ prime (nat p); odd p ⟧ ⟹
∃ t. 0<t ∧ t<p ∧ is_sum4sq_int (p*t)"
proof -
assume p1: "prime (nat p)"
then have p0: "p > 1" and "prime p"
by (simp_all add: prime_int_nat_transfer prime_nat_iff)
assume p2: "odd p"
then obtain n where n: "p = 2*n+1" using oddE by blast
with p1 have n0: "n > 0" by (auto simp add: prime_nat_iff)
let ?C = "{0 ..< p}"
let ?D = "{0 .. n}"
let ?f = "%x. x^2 mod p"
let ?g = "%x. (-1-x^2) mod p"
let ?A = "?f ` ?D"
let ?B = "?g ` ?D"
have finC: "finite ?C" by simp
have finD: "finite ?D" by simp
from p0 have AsubC: "?A ⊆ ?C" and BsubC: "?B ⊆ ?C"
by auto
with finC have finA: "finite ?A" and finB: "finite ?B"
by (auto simp add: finite_subset)
from AsubC BsubC have AunBsubC: "?A ∪ ?B ⊆ ?C" by (rule Un_least)
from p0 have cardC: "card ?C = nat p" using card_atLeastZeroLessThan_int by blast
from n0 have cardD: "card ?D = 1+ nat n" by simp
have cardA: "card ?A = card ?D"
proof -
have "inj_on ?f ?D"
proof (unfold inj_on_def, auto)
fix x fix y
assume x0: "0 ≤ x" and xn: "x ≤ n" and y0: "0 ≤ y" and yn: " y ≤ n"
and xyp: "x^2 mod p = y^2 mod p"
with p0 have "[x^2 = y^2] (mod p)" using cong_def by blast
hence "p dvd x^2-y^2" using cong_iff_dvd_diff by blast
hence "p dvd (x+y)*(x-y)" by (simp add: power2_eq_square algebra_simps)
hence "p dvd x+y ∨ p dvd x-y" using ‹prime p› p0
by (auto dest: prime_dvd_multD)
moreover
{ assume "p dvd x+y"
moreover from xn yn n have "x+y < p" by auto
ultimately have "¬ x+y > 0" by (auto simp add: zdvd_not_zless)
with x0 y0 have "x = y" by auto }
moreover
{ assume ass: "p dvd x-y"
have "x = y"
proof (rule ccontr, case_tac "x-y ≥ 0")
assume "x-y ≥ 0" and "x ≠ y" hence "x-y > 0" by auto
with ass have "¬ x-y < p" by (auto simp add: zdvd_not_zless)
with xn y0 n p0 show "False" by auto
next
assume "¬ 0 ≤ x-y" hence "y-x > 0" by auto
moreover from x0 yn n p0 have "y-x < p" by auto
ultimately have "¬ p dvd y-x" by (auto simp add: zdvd_not_zless)
moreover from ass have "p dvd -(x-y)" by (simp only: dvd_minus_iff)
ultimately show "False" by auto
qed }
ultimately show "x=y" by auto
qed
with finD show ?thesis by (simp only: inj_on_iff_eq_card)
qed
have cardB: "card ?B = card ?D"
proof -
have "inj_on ?g ?D"
proof (unfold inj_on_def, auto)
fix x fix y
assume x0: "0 ≤ x" and xn: "x ≤ n" and y0: "0 ≤ y" and yn: " y ≤ n"
and xyp: "(-1-x^2) mod p = (-1-y^2) mod p"
with p0 have "[-1-y^2 = -1-x^2] (mod p)" by (simp only: cong_def)
hence "p dvd (-1-y^2) - (-1-x^2)" by (simp only: cong_iff_dvd_diff)
moreover have "-1-y^2 - (-1-x^2) = x^2 - y^2" by arith
ultimately have "p dvd x^2-y^2" by simp
hence "p dvd (x+y)*(x-y)" by (simp add: power2_eq_square algebra_simps)
with p1 have "p dvd x+y ∨ p dvd x-y" using ‹prime p› p0
by (auto dest: prime_dvd_multD)
moreover
{ assume "p dvd x+y"
moreover from xn yn n have "x+y < p" by auto
ultimately have "¬ x+y > 0" by (auto simp add: zdvd_not_zless)
with x0 y0 have "x = y" by auto }
moreover
{ assume ass: "p dvd x-y"
have "x = y"
proof (rule ccontr, case_tac "x-y ≥ 0")
assume "x-y ≥ 0" and "x ≠ y" hence "x-y > 0" by auto
with ass have "¬ x-y < p" by (auto simp add: zdvd_not_zless)
with xn y0 n p0 show "False" by auto
next
assume "¬ 0 ≤ x-y" hence "y-x > 0" by auto
moreover from x0 yn n p0 have "y-x < p" by auto
ultimately have "¬ p dvd y-x" by (auto simp add: zdvd_not_zless)
moreover from ass have "p dvd -(x-y)" by (simp only: dvd_minus_iff)
ultimately show "False" by auto
qed }
ultimately show "x=y" by auto
qed
with finD show ?thesis by (simp only: inj_on_iff_eq_card)
qed
have "?A ∩ ?B ≠ {}"
proof (rule ccontr, auto)
assume ABdisj: "?A ∩ ?B = {}"
from cardA cardB cardD have "2 + 2*(nat n) = card ?A + card ?B" by auto
also with finA finB ABdisj have "… = card (?A ∪ ?B)"
by (simp only: card_Un_disjoint)
also with finC AunBsubC have "… ≤ card ?C" by (simp only: card_mono)
also with cardC have "… = nat p" by simp
finally have "2 + 2*(nat n) ≤ nat p" by simp
with n show "False" by arith
qed
then obtain z where "z ∈ ?A ∧ z ∈ ?B" by auto
then obtain x y where xy: "x ∈ ?D ∧ y ∈ ?D ∧ z = x^2 mod p ∧ z = (-1-y^2) mod p" by blast
with p0 have "[x^2=-1-y^2](mod p)" by (simp add: cong_def)
hence "p dvd x^2-(-1-y^2)" by (simp only: cong_iff_dvd_diff)
moreover have "x^2-(-1-y^2)=x^2+y^2+1" by arith
ultimately have "p dvd sum4sq_int(x,y,1,0)" by (auto simp add: sum4sq_int_def)
then obtain t where t: "p * t = sum4sq_int(x,y,1,0)" by (auto simp only: dvd_def eq_refl)
hence "is_sum4sq_int (p*t)" by (unfold is_sum4sq_int_def, auto)
moreover have "t > 0 ∧ t < p"
proof
have "x^2 ≥ 0 ∧ y^2 ≥ 0" by simp
hence "x^2+y^2+1 > 0" by arith
with t have "p*t > 0" by (unfold sum4sq_int_def, auto)
moreover
{ assume "t < 0" with p0 have "p*t < p*0" by (simp only: zmult_zless_mono2)
hence "p*t < 0" by simp }
moreover
{ assume "t = 0" hence "p*t = 0" by simp }
ultimately have "¬ t < 0 ∧ t ≠ 0" by auto
thus "t > 0" by simp
from xy have "x^2 ≤ n^2 ∧ y^2 ≤ n^2" by (auto simp add: power_mono)
hence "x^2+y^2+1 ≤ 2*n^2 + 1" by auto
with t have contr: "p*t ≤ 2*n^2+1" by (simp add: sum4sq_int_def)
moreover
{ assume "t > n+1"
with p0 have "p*(n+1) < p*t" by (simp only: zmult_zless_mono2)
with n have "p*t > (2*n+1)*n + (2*n+1)*1" by (simp only: distrib_left)
hence "p*t > 2*n*n + n + 2*n + 1" by (simp only: distrib_right mult_1_left)
with n0 have "p*t > 2*n^2 + 1" by (simp add: power2_eq_square) }
ultimately have "¬ t > n+1" by auto
with n0 n show "t < p" by auto
qed
ultimately show ?thesis by blast
qed
private lemma zprime_is_sum4sq: "prime (nat p) ⟹ is_sum4sq_int p"
proof (cases)
assume p2: "p=2"
hence "p = sum4sq_int(1,1,0,0)" by (auto simp add: sum4sq_int_def)
thus ?thesis by (auto simp add: is_sum4sq_int_def)
next
assume "¬ p =2" and prp: "prime (nat p)"
hence "¬ nat p = 2" by simp
with prp have "2 < nat p" using prime_nat_iff by force
moreover with prp have "odd (nat p)" using prime_odd_nat[of "nat p"] by blast
ultimately have "odd p" by (simp add: even_nat_iff)
with prp have "∃ t. 0<t ∧ t<p ∧ is_sum4sq_int (p*t)" by (rule mult_oddprime_is_sum4sq)
then obtain a b c d t where pt_sol: "0<t ∧ t<p ∧ p*t = sum4sq_int(a,b,c,d)"
by (unfold is_sum4sq_int_def, blast)
hence Qt: "0<t ∧ t<p ∧ (∃ a1 a2 a3 a4. p*t = sum4sq_int(a1,a2,a3,a4))"
(is "?Q t") by blast
have "?Q 1"
proof (rule ccontr)
assume nQ1: "¬ ?Q 1"
have "¬ ?Q t"
proof (induct t rule: infinite_descent0_measure[where V="λx. (nat x)- 1"], clarify)
fix x a b c d
assume "nat x - 1 = 0" and "x > 0" and s: "p*x=sum4sq_int(a,b,c,d)" and "x < p"
moreover hence "x = 1" by arith
ultimately have "?Q 1" by auto
with nQ1 show False by auto
next
fix x
assume "0 < nat x - 1" and "¬ ¬ ?Q x"
then obtain a1 a2 a3 a4 where ass: "1<x ∧ x<p ∧ p*x = sum4sq_int(a1,a2,a3,a4)"
by auto
have "∃ y. nat y - 1 < nat x - 1 ∧ ?Q y"
proof (cases)
assume evx: "even x"
hence "even (x*p)" by simp
with ass have ev1234: "even (a1^2+a2^2 + a3^2+a4^2)"
by (auto simp add: sum4sq_int_def ac_simps)
have "∃ b1 b2 b3 b4. p*x=sum4sq_int(b1,b2,b3,b4) ∧ even (b1+b2) ∧ even (b3+b4)"
proof (cases)
assume ev12: "even (a1^2+a2^2)"
with ev1234 ass show ?thesis by auto
next
assume "¬ even (a1^2+a2^2)"
hence odd12: "odd (a1^2+a2^2)" by simp
with ev1234 have odd34: "odd (a3^2+a4^2)" by auto
show ?thesis
proof (cases)
assume ev1: "even (a1^2)"
with odd12 have odd2: "odd (a2^2)" by simp
show ?thesis
proof (cases)
assume "even (a3^2)"
moreover from ass have "p*x = sum4sq_int(a1,a3,a2,a4)" by (auto simp add: sum4sq_int_def)
ultimately show ?thesis using odd2 odd34 ev1 by auto
next
assume "¬ even (a3^2)"
moreover from ass have "p*x = sum4sq_int(a1,a4,a2,a3)" by (auto simp add: sum4sq_int_def)
ultimately show ?thesis using odd34 odd2 ev1 by auto
qed
next
assume odd1: "¬ even (a1^2)"
with odd12 have ev2: "even (a2^2)" by simp
show ?thesis
proof (cases)
assume "even (a3^2)"
moreover from ass have "sum4sq_int(a1,a4,a2,a3)=p*x" by (auto simp add: sum4sq_int_def)
ultimately show ?thesis using odd34 odd1 ev2 by force
next
assume "¬ even (a3^2)"
moreover from ass have "sum4sq_int(a1,a3,a2,a4)=p*x" by (auto simp add: sum4sq_int_def)
ultimately show ?thesis using odd34 odd1 ev2 by force
qed
qed
qed
then obtain b1 b2 b3 b4
where b: "p*x = sum4sq_int(b1,b2,b3,b4) ∧ even (b1+b2) ∧ even (b3+b4)" by auto
then obtain c1 c3 where c13: "b1+b2 = 2*c1 ∧ b3+b4 = 2*c3"
using evenE[of "b1+b2"] evenE[of "b3+b4"] by meson
from b have "even (b1-b2) ∧ even (b3-b4)" by simp
then obtain c2 c4 where c24: "b1-b2 = 2*c2 ∧ b3-b4 = 2*c4"
using evenE[of "b1-b2"] evenE[of "b3-b4"] by meson
from evx obtain y where y: "x = 2*y" using evenE by blast
hence "4*(p*y) = 2*(p*x)" by (simp add: ac_simps)
also from b have "… = 2*b1^2 + 2*b2^2 + 2*b3^2 + 2*b4^2"
by (auto simp: sum4sq_int_def)
also have "… = (b1 + b2)^2 + (b1 - b2)^2 + (b3 + b4)^2 + (b3 - b4)^2"
by (auto simp add: power2_eq_square algebra_simps)
also with c13 c24 have "… = 4*(c1^2 + c2^2 + c3^2 + c4^2)"
by (auto simp add: power_mult_distrib)
finally have "p * y = sum4sq_int(c1,c2,c3,c4)" by (auto simp add: sum4sq_int_def)
moreover from y ass have "0 < y ∧ y < p ∧ (nat y) - 1 < (nat x) - 1" by arith
ultimately show ?thesis by blast
next
assume xodd: "¬ even x"
with ass have "∃ c1 c2 c3 c4. 2*¦a1-c1*x¦≤x ∧ 2*¦a2-c2*x¦≤x ∧ 2*¦a3-c3*x¦≤x ∧ 2*¦a4-c4*x¦≤x"
by (simp add: best_division_abs)
then obtain b1 c1 b2 c2 b3 c3 b4 c4 where
bc_def: "b1 = a1-c1*x ∧ b2 = a2-c2*x ∧ b3 = a3-c3*x ∧ b4 = a4-c4*x"
and "2*¦b1¦≤x ∧ 2*¦b2¦≤x ∧ 2*¦b3¦≤x ∧ 2*¦b4¦≤x"
by blast
moreover have "2*¦b1¦≠x ∧ 2*¦b2¦≠x ∧ 2*¦b3¦≠x ∧ 2*¦b4¦≠x" using xodd by fastforce
ultimately have bc_abs: "2*¦b1¦<x ∧ 2*¦b2¦<x ∧ 2*¦b3¦<x ∧ 2*¦b4¦<x" by auto
let ?B = "b1^2 + b2^2 + b3^2 + b4^2"
let ?C = "c1^2 + c2^2 + c3^2 + c4^2"
have "x dvd ?B"
proof
from bc_def ass have
"?B = p*x - 2*(a1*c1+a2*c2+a3*c3+a4*c4)*x + ?C*x^2"
unfolding sum4sq_int_def by (auto simp add: power2_eq_square algebra_simps)
thus "?B = x*(p - 2*(a1*c1+a2*c2+a3*c3+a4*c4) + ?C*x)"
by (auto simp add: ac_simps power2_eq_square
distrib_left right_diff_distrib)
qed
then obtain y where y: "?B = x * y" by (auto simp add: dvd_def)
let ?A1 = "a1*b1 + a2*b2 + a3*b3 + a4*b4"
let ?A2 = "a1*b2 - a2*b1 - a3*b4 + a4*b3"
let ?A3 = "a1*b3 + a2*b4 - a3*b1 - a4*b2"
let ?A4 = "a1*b4 - a2*b3 + a3*b2 - a4*b1"
let ?A = "sum4sq_int(?A1,?A2,?A3,?A4)"
have "x dvd ?A1 ∧ x dvd ?A2 ∧ x dvd ?A3 ∧ x dvd ?A4"
proof (safe)
from bc_def have
"?A1 = (b1+c1*x)*b1 + (b2+c2*x)*b2 + (b3+c3*x)*b3 + (b4+c4*x)*b4"
by simp
also with y have "… = x*(y + c1*b1 + c2*b2 + c3*b3 + c4*b4)"
by (auto simp add: distrib_left power2_eq_square ac_simps)
finally show "x dvd ?A1" by auto
from bc_def have
"?A2 = (b1+c1*x)*b2 - (b2+c2*x)*b1 - (b3+c3*x)*b4 + (b4+c4*x)*b3"
by simp
also have "… = x*(c1*b2 - c2*b1 - c3*b4 + c4*b3)"
by (auto simp add: distrib_left right_diff_distrib ac_simps)
finally show "x dvd ?A2" by auto
from bc_def have
"?A3 = (b1+c1*x)*b3 + (b2+c2*x)*b4 - (b3+c3*x)*b1 - (b4+c4*x)*b2"
by simp
also have "… = x*(c1*b3 + c2*b4 - c3*b1 - c4*b2)"
by (auto simp add: distrib_left right_diff_distrib ac_simps)
finally show "x dvd ?A3" by auto
from bc_def have
"?A4 = (b1+c1*x)*b4 - (b2+c2*x)*b3 + (b3+c3*x)*b2 - (b4+c4*x)*b1"
by simp
also have "… = x*(c1*b4 - c2*b3 + c3*b2 - c4*b1)"
by (auto simp add: distrib_left right_diff_distrib ac_simps)
finally show "x dvd ?A4" by auto
qed
then obtain d1 d2 d3 d4 where d:
"?A1=x*d1 ∧ ?A2=x*d2 ∧ ?A3=x*d3 ∧ ?A4=x*d4"
by (auto simp add: dvd_def)
let ?D = "sum4sq_int(d1,d2,d3,d4)"
from d have "x^2*?D = ?A"
by (auto simp only: sum4sq_int_def power_mult_distrib distrib_left)
also have "… = sum4sq_int(a1,a2,a3,a4)*sum4sq_int(b1,b2,b3,b4)"
by (simp only: mult_sum4sq_int)
also with y ass have "… = (p*x)*(x*y)" by (auto simp add: sum4sq_int_def)
also have "… = x^2*(p*y)" by (simp only: power2_eq_square ac_simps)
finally have "x^2*(?D - p*y) = 0" by (auto simp add: right_diff_distrib)
with ass have "p*y = ?D" by auto
moreover have y_l_x: "y < x"
proof -
have "4*b1^2 = (2*¦b1¦)^2 ∧ 4*b2^2 = (2*¦b2¦)^2 ∧
4*b3^2 = (2*¦b3¦)^2 ∧ 4*b4^2 = (2*¦b4¦)^2" by simp
with bc_abs have "4*b1^2<x^2 ∧ 4*b2^2<x^2 ∧ 4*b3^2<x^2 ∧ 4*b4^2<x^2"
using power_strict_mono [of "2*¦b¦" x 2 for b]
by auto
hence "?B < x^2" by auto
with y have "x*(x-y) > 0"
by (auto simp add: power2_eq_square right_diff_distrib)
moreover from ass have "x > 0" by simp
ultimately show ?thesis using zero_less_mult_pos by fastforce
qed
moreover have "y > 0"
proof -
have b2pos: "b1^2 ≥ 0 ∧ b2^2 ≥ 0 ∧ b3^2 ≥ 0 ∧ b4^2 ≥ 0" by simp
hence "?B = 0 ∨ ?B > 0" by arith
moreover
{ assume "?B = 0"
moreover from b2pos have
"?B-b1^2 ≥ 0 ∧ ?B-b2^2 ≥ 0 ∧ ?B-b3^2 ≥ 0 ∧ ?B-b4^2 ≥ 0" by arith
ultimately have "b1^2 ≤ 0 ∧ b2^2 ≤ 0 ∧ b3^2 ≤ 0 ∧ b4^2 ≤ 0" by auto
with b2pos have "b1^2 = 0 ∧ b2^2 = 0 ∧ b3^2 = 0 ∧ b4^2 = 0" by arith
hence "b1 = 0 ∧ b2 = 0 ∧ b3 = 0 ∧ b4 = 0" by auto
with bc_def have "x dvd a1 ∧ x dvd a2 ∧ x dvd a3 ∧ x dvd a4"
by auto
hence "x^2 dvd a1^2 ∧ x^2 dvd a2^2 ∧ x^2 dvd a3^2 ∧ x^2 dvd a4^2" by simp
hence "x^2 dvd a1^2+a2^2+a3^2+a4^2" by (simp only: dvd_add)
with ass have "x^2 dvd p*x" by (auto simp only: sum4sq_int_def)
hence "x*x dvd x*p" by (simp only: power2_eq_square ac_simps)
with ass have "nat x dvd nat p"
by (simp add: nat_dvd_iff)
moreover from ass prp have "x ≥ 0 ∧ x ≠ 1 ∧ x ≠ p ∧ prime (nat p)" by simp
ultimately have "False" unfolding prime_nat_iff by auto }
moreover
{ assume "?B > 0"
with y have "x*y > 0" by simp
moreover from ass have "x > 0" by simp
ultimately have ?thesis using zero_less_mult_pos by blast }
ultimately show ?thesis by auto
qed
moreover with y_l_x have "(nat y) - 1 < (nat x) - 1" by arith
moreover from y_l_x ass have "y < p" by auto
ultimately show ?thesis by blast
qed
thus "∃ y. nat y - 1 < nat x - 1 ∧ ¬ ¬ ?Q y" by blast
qed
with Qt show "False" by simp
qed
thus "is_sum4sq_int p" by (auto simp add: is_sum4sq_int_def)
qed
private lemma prime_is_sum4sq: "prime p ⟹ is_sum4sq_nat p"
using zprime_is_sum4sq is_sum4sq_int_nat_eq by simp
theorem sum_of_four_squares: "is_sum4sq_nat n"
proof (induction n rule: nat_less_induct)
case (1 n)
show ?case
proof (cases "n>1")
case False
hence "n = 0 ∨ n = 1" by auto
moreover have "0 = sum4sq_nat 0 0 0 0" "1 = sum4sq_nat 1 0 0 0" unfolding sum4sq_nat_def by auto
ultimately show ?thesis unfolding is_sum4sq_nat_def by blast
next
case True
then obtain p m where dec: "prime p ∧ n = p * m" using prime_factor_nat[of n]
by (auto elim: dvdE)
moreover hence "m<n" using n_less_m_mult_n[of m p] prime_gt_Suc_0_nat[of p] True by linarith
ultimately have "is_sum4sq_nat m" "is_sum4sq_nat p" using 1 prime_is_sum4sq by blast+
thus ?thesis using dec is_mult_sum4sq_nat by blast
qed
qed
end
end