From ed68ab3d6a62ca827d5d9fce0b5ff019ba637d40 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Mon, 6 Jan 2025 23:36:40 -0500
Subject: [PATCH] The formula for the distance of squares

---
 .../fermat-numbers.lagda.md                   |  2 +-
 .../multiplication-natural-numbers.lagda.md   | 10 ++++
 .../squares-natural-numbers.lagda.md          | 58 +++++++++++++++++++
 3 files changed, 69 insertions(+), 1 deletion(-)

diff --git a/src/elementary-number-theory/fermat-numbers.lagda.md b/src/elementary-number-theory/fermat-numbers.lagda.md
index 3e169f638b..d753d37a77 100644
--- a/src/elementary-number-theory/fermat-numbers.lagda.md
+++ b/src/elementary-number-theory/fermat-numbers.lagda.md
@@ -98,7 +98,7 @@ compute-succ-recursive-fermat-number-ℕ =
 
 ## Properties
 
-### The Fermat number at a successor
+### The Fermat number of a successor
 
 Any Fermat number of the form $F(n+1)=2^{2^{n+1}}+1$ can be computed as
 
diff --git a/src/elementary-number-theory/multiplication-natural-numbers.lagda.md b/src/elementary-number-theory/multiplication-natural-numbers.lagda.md
index 0cc4824158..fbee2ce1fd 100644
--- a/src/elementary-number-theory/multiplication-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/multiplication-natural-numbers.lagda.md
@@ -183,6 +183,16 @@ abstract
     ( ( left-distributive-mul-add-ℕ z x y) ∙
       ( ( ap (_+ℕ (z *ℕ y)) (commutative-mul-ℕ z x)) ∙
         ( ap ((x *ℕ z) +ℕ_) (commutative-mul-ℕ z y))))
+
+abstract
+  double-distributive-mul-add-ℕ :
+    (w x y z : ℕ) → (w +ℕ x) *ℕ (y +ℕ z) ＝ w *ℕ y +ℕ w *ℕ z +ℕ x *ℕ y +ℕ x *ℕ z
+  double-distributive-mul-add-ℕ w x y z =
+    ( right-distributive-mul-add-ℕ w x (y +ℕ z)) ∙
+    ( ap-add-ℕ
+      ( left-distributive-mul-add-ℕ w y z)
+      ( left-distributive-mul-add-ℕ x y z)) ∙
+    ( inv (associative-add-ℕ (w *ℕ y +ℕ w *ℕ z) (x *ℕ y) (x *ℕ z)))
 ```
 
 ### Multiplication is associative
diff --git a/src/elementary-number-theory/squares-natural-numbers.lagda.md b/src/elementary-number-theory/squares-natural-numbers.lagda.md
index 7a9d7077d9..2e8fa31dda 100644
--- a/src/elementary-number-theory/squares-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/squares-natural-numbers.lagda.md
@@ -559,6 +559,64 @@ module _
       ( bounded-div-square-ℕ)
 ```
 
+### Squares of sums of natural numbers
+
+```agda
+square-add-ℕ :
+  (m n : ℕ) → square-ℕ (m +ℕ n) ＝ square-ℕ m +ℕ 2 *ℕ (m *ℕ n) +ℕ square-ℕ n
+square-add-ℕ m n =
+  ( double-distributive-mul-add-ℕ m n m n) ∙
+  ( ap
+    ( _+ℕ square-ℕ n)
+    ( ( associative-add-ℕ (square-ℕ m) (m *ℕ n) (n *ℕ m)) ∙
+      ( ap
+        ( square-ℕ m +ℕ_)
+        ( ( ap (m *ℕ n +ℕ_) (commutative-mul-ℕ n m)) ∙
+          ( inv (left-two-law-mul-ℕ (m *ℕ n)))))))
+```
+
+### The formula for the distance between squares
+
+The formula for the distance between squares is more commonly known as the formula for the difference of squares. However, since we prefer using the distance operation on the natural numbers over the partial difference operation, we will state and prove the analogous formula using the distance function.
+
+The formula for the difference of squares of integers is formalized in its usual form.
+
+```agda
+distance-of-squares-ℕ' :
+  (m n k : ℕ) → m +ℕ k ＝ n →
+  dist-ℕ (square-ℕ m) (square-ℕ n) ＝ dist-ℕ m n *ℕ (m +ℕ n)
+distance-of-squares-ℕ' m ._ k refl =
+  ( ap
+    ( dist-ℕ (square-ℕ m))
+    ( ( square-add-ℕ m k) ∙
+      ( associative-add-ℕ (square-ℕ m) (2 *ℕ (m *ℕ k)) (square-ℕ k)))) ∙
+  ( dist-add-ℕ (square-ℕ m) (2 *ℕ (m *ℕ k) +ℕ square-ℕ k)) ∙
+  ( ap
+    ( _+ℕ square-ℕ k)
+    ( inv (associative-mul-ℕ 2 m k) ∙ ap (_*ℕ k) (left-two-law-mul-ℕ m))) ∙
+  ( inv (right-distributive-mul-add-ℕ (m +ℕ m) k k)) ∙
+  ( ap (_*ℕ k) (associative-add-ℕ m m k)) ∙
+  ( commutative-mul-ℕ (m +ℕ (m +ℕ k)) k) ∙
+  ( ap (_*ℕ (m +ℕ (m +ℕ k))) (inv (dist-add-ℕ m k)))
+
+abstract
+  distance-of-squares-ℕ :
+    (m n : ℕ) → dist-ℕ (square-ℕ m) (square-ℕ n) ＝ dist-ℕ m n *ℕ (m +ℕ n)
+  distance-of-squares-ℕ m n
+    with
+    linear-leq-ℕ m n
+  ... | inl H =
+    distance-of-squares-ℕ' m n
+      ( pr1 (subtraction-leq-ℕ m n H))
+      ( commutative-add-ℕ m _ ∙ pr2 (subtraction-leq-ℕ m n H))
+  ... | inr H =
+    ( symmetric-dist-ℕ (square-ℕ m) (square-ℕ n)) ∙
+    ( distance-of-squares-ℕ' n m
+      ( pr1 (subtraction-leq-ℕ n m H))
+      ( commutative-add-ℕ n _ ∙ pr2 (subtraction-leq-ℕ n m H))) ∙
+    ( ap-mul-ℕ (symmetric-dist-ℕ n m) (commutative-add-ℕ n m))
+```
+
 ### The $n$th square is the sum of the first $n$ odd numbers
 
 We show that