From ae9a6330372c0cc2aff9bcb5ac1eedefccc0602c Mon Sep 17 00:00:00 2001
From: oxe-i <oxe-b@gmail.com>
Date: Sun, 15 Mar 2026 09:04:23 -0300
Subject: [PATCH 1/3] add approaches and article to difference-of-squares

---
 .../.approaches/config.json                   |  35 +++
 .../.approaches/folding-over-range/content.md |  63 +++++
 .../folding-over-range/snippet.txt            |   6 +
 .../.approaches/introduction.md               |  75 ++++++
 .../mathematical-formula/content.md           |  27 ++
 .../mathematical-formula/snippet.txt          |   5 +
 .../.approaches/recurse-numbers/content.md    |  85 ++++++
 .../.approaches/recurse-numbers/snippet.txt   |   8 +
 .../.articles/config.json                     |  13 +
 .../content.md                                | 244 ++++++++++++++++++
 .../snippet.md                                |   8 +
 11 files changed, 569 insertions(+)
 create mode 100644 exercises/practice/difference-of-squares/.approaches/config.json
 create mode 100644 exercises/practice/difference-of-squares/.approaches/folding-over-range/content.md
 create mode 100644 exercises/practice/difference-of-squares/.approaches/folding-over-range/snippet.txt
 create mode 100644 exercises/practice/difference-of-squares/.approaches/introduction.md
 create mode 100644 exercises/practice/difference-of-squares/.approaches/mathematical-formula/content.md
 create mode 100644 exercises/practice/difference-of-squares/.approaches/mathematical-formula/snippet.txt
 create mode 100644 exercises/practice/difference-of-squares/.approaches/recurse-numbers/content.md
 create mode 100644 exercises/practice/difference-of-squares/.approaches/recurse-numbers/snippet.txt
 create mode 100644 exercises/practice/difference-of-squares/.articles/config.json
 create mode 100644 exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md
 create mode 100644 exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/snippet.md

diff --git a/exercises/practice/difference-of-squares/.approaches/config.json b/exercises/practice/difference-of-squares/.approaches/config.json
new file mode 100644
index 0000000..650d318
--- /dev/null
+++ b/exercises/practice/difference-of-squares/.approaches/config.json
@@ -0,0 +1,35 @@
+{
+  "introduction": {
+    "authors": ["oxe-i"],
+    "contributors": []
+  },
+  "approaches": [
+    {
+      "uuid": "854dac53-adfd-46ad-8c64-46e401a46a37",
+      "slug": "recurse-numbers",
+      "title": "Recurse Over Numbers",
+      "blurb": "recurse over all numbers to sum them up.",
+      "authors": [
+        "oxe-i"
+      ]
+    },
+    {
+      "uuid": "3e4413e6-89cb-4e1e-8e83-89e84754dd0f",
+      "slug": "mathematical-formula",
+      "title": "Mathematical Formula",
+      "blurb": "calculate sums using known mathematical formulas.",
+      "authors": [
+        "oxe-i"
+      ]
+    },
+    {
+      "uuid": "0e48332a-1b9b-4322-b941-933d1c718d67",
+      "slug": "folding-over-range",
+      "title": "Folding Over Range",
+      "blurb": "use a fold to sum all numbers in a range.",
+      "authors": [
+        "oxe-i"
+      ]
+    }
+  ]
+}
diff --git a/exercises/practice/difference-of-squares/.approaches/folding-over-range/content.md b/exercises/practice/difference-of-squares/.approaches/folding-over-range/content.md
new file mode 100644
index 0000000..1f7121c
--- /dev/null
+++ b/exercises/practice/difference-of-squares/.approaches/folding-over-range/content.md
@@ -0,0 +1,63 @@
+# Folding Over Range
+
+In functional programming languages, a [fold][fold] is a common way to iterate over a collection while accumulating a result.
+
+A fold processes the elements of a collection one by one, updating an accumulator at each step. 
+To perform a fold, three things are needed:
+
+1. A collection of elements, often stored in a `List` or an `Array`.
+2. An initial value for the accumulator.
+3. A function that combines the current element with the accumulator to produce a new accumulator.
+
+For example, if we fold a collection of numbers using `0` as the initial value and addition as the combining function, the result will be the sum of all elements in the collection.
+
+Lean provides helper functions for `List` and `Array` that generate collections of sequential numbers, which can then be processed with a fold:
+
+```lean
+def squareOfSum (number : Nat) : Nat :=
+    let sum := (List.range' 1 number).foldl (fun acc x => acc + x) 0
+    sum ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    (List.range' 1 number).foldl (init := 0) fun acc x => acc + x^2
+
+def differenceOfSquares (number : Nat) : Nat := (squareOfSum number) - (sumOfSquares number)
+```
+
+Both [List.range'][list-range'] and [Array.range'][array-range'] create collections of consecutive natural numbers.
+They take:
+
+- a starting value (the first argument, `1` in the example), and
+- a count (the second argument, `number`).
+
+The result is a collection containing `number` values starting from the initial value.
+
+An optional third argument specifies the _step size_, which determines how much each value increases relative to the previous one. 
+If omitted, the default step is `1`, producing consecutive numbers.
+
+Lean also defines a [fold directly for `Nat`][nat-fold]. 
+Instead of folding over an explicit collection, this function iterates from `0` up to (but not including) a given number.
+
+The folding function receives three arguments:
+
+1. the current index,
+2. a proof that the index is less than the bound, and
+3. the current accumulator.
+
+```lean
+def squareOfSum (number : Nat) : Nat :=
+    let sum := number.fold (init := 0) fun i _ acc => (i + 1) + acc
+    sum ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    number.fold (fun i _ acc => acc + (i + 1) ^ 2) 0
+
+def differenceOfSquares (number : Nat) : Nat := (squareOfSum number) - (sumOfSquares number)
+```
+
+This approach avoids explicitly creating a collection and instead performs the iteration directly over the natural numbers, which can be more efficient.
+
+[fold]: https://en.wikipedia.org/wiki/Fold_(higher-order_function)
+[list-range']: https://lean-lang.org/doc/reference/latest/Basic-Types/Linked-Lists/#List___range___
+[array-range']: https://lean-lang.org/doc/reference/latest/Basic-Types/Arrays/#Array___range___
+[nat-fold]: https://lean-lang.org/doc/reference/latest/Basic-Types/Natural-Numbers/#Nat___fold
diff --git a/exercises/practice/difference-of-squares/.approaches/folding-over-range/snippet.txt b/exercises/practice/difference-of-squares/.approaches/folding-over-range/snippet.txt
new file mode 100644
index 0000000..f37cb2b
--- /dev/null
+++ b/exercises/practice/difference-of-squares/.approaches/folding-over-range/snippet.txt
@@ -0,0 +1,6 @@
+def squareOfSum (number : Nat) : Nat :=
+    let sum := number.fold (init := 0) fun i _ acc => (i + 1) + acc
+    sum ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    number.fold (fun i _ acc => acc + (i + 1) ^ 2) 0
diff --git a/exercises/practice/difference-of-squares/.approaches/introduction.md b/exercises/practice/difference-of-squares/.approaches/introduction.md
new file mode 100644
index 0000000..f788756
--- /dev/null
+++ b/exercises/practice/difference-of-squares/.approaches/introduction.md
@@ -0,0 +1,75 @@
+# Introduction
+
+There are multiple ways to solve `difference-of-squares`.
+Some of them include:
+
+* Recursing over numbers.
+* Using known mathematical formulas.
+* Folding over a range of numbers.
+
+## Approach: Recursing over numbers
+
+Recurse over decreasing numbers until a base case is reached, accumulating the result:
+
+```lean
+def sumN (n : Nat) (acc : Nat) : Nat :=
+    if n = 0 
+    then acc 
+    else sumN (n - 1) (acc + n)
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumN number 0) ^ 2
+
+def sumSquareN (n : Nat) (acc : Nat) : Nat :=
+    if n = 0 
+    then acc 
+    else sumSquareN (n - 1) (acc + (n ^ 2))
+
+def sumOfSquares (number : Nat) : Nat :=
+    sumSquareN number 0
+
+def differenceOfSquares (number : Nat) : Nat := (squareOfSum number) - (sumOfSquares number)
+```
+
+For more details, see the [recurse-numbers][recurse-numbers] approach.
+
+## Approach: Using mathematical formulas
+
+Compute the results directly using mathematical formulas:
+
+```lean
+def sumFirstNPositive (n : Nat) : Nat :=
+    n * (n + 1) / 2
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumFirstNPositive number) ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    (number * (number + 1) * (2 * number + 1)) / 6
+
+def differenceOfSquares (number : Nat) : Nat :=
+    (squareOfSum number) - (sumOfSquares number)
+```
+
+For more details, see the [mathematical-formula][mathematical-formula] approach.
+
+## Approach: Folding over range
+
+Use a `fold` to iterate over a range of values and accumulate the result:
+
+```lean
+def squareOfSum (number : Nat) : Nat :=
+    let sum := number.fold (init := 0) fun i _ acc => (i + 1) + acc
+    sum ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    number.fold (fun i _ acc => acc + (i + 1) ^ 2) 0
+
+def differenceOfSquares (number : Nat) : Nat := (squareOfSum number) - (sumOfSquares number)
+```
+
+For more details, see the [folding-over-range][folding-over-range] approach.
+
+[recurse-numbers]: https://exercism.org/tracks/lean/exercises/difference-of-squares/approaches/recurse-numbers
+[mathematical-formula]: https://exercism.org/tracks/lean/exercises/difference-of-squares/approaches/mathematical-formula
+[folding-over-range]: https://exercism.org/tracks/lean/exercises/difference-of-squares/approaches/folding-over-range
diff --git a/exercises/practice/difference-of-squares/.approaches/mathematical-formula/content.md b/exercises/practice/difference-of-squares/.approaches/mathematical-formula/content.md
new file mode 100644
index 0000000..5ca3519
--- /dev/null
+++ b/exercises/practice/difference-of-squares/.approaches/mathematical-formula/content.md
@@ -0,0 +1,27 @@
+# Mathematical Formula
+
+A possible way to solve this exercise is to use [known mathematical formulas][formulas]:
+
+* The sum of positive integers up to `n`, inclusive, is `n * (n + 1) / 2`.
+  Squaring that sum gives `squareOfSum`.
+* The sum of the squares of positive integers up to `n`, inclusive, is `n * (n + 1) * (2 * n + 1) / 6`.
+
+```lean
+def sumFirstNPositive (n : Nat) : Nat :=
+    n * (n + 1) / 2
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumFirstNPositive number) ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    (number * (number + 1) * (2 * number + 1)) / 6
+
+def differenceOfSquares (number : Nat) : Nat :=
+    (squareOfSum number) - (sumOfSquares number)
+```
+
+This is probably the most efficient approach, since the problem reduces to a few constant multiplications and divisions, whereas the other approaches are `O(n)`.
+On the other hand, the solution becomes more opaque because these formulas are not obvious from the structure of the problem. 
+They require previous knowledge or further research.
+
+[formulas]: https://en.wikipedia.org/wiki/Triangular_number
diff --git a/exercises/practice/difference-of-squares/.approaches/mathematical-formula/snippet.txt b/exercises/practice/difference-of-squares/.approaches/mathematical-formula/snippet.txt
new file mode 100644
index 0000000..23fec37
--- /dev/null
+++ b/exercises/practice/difference-of-squares/.approaches/mathematical-formula/snippet.txt
@@ -0,0 +1,5 @@
+def squareOfSum (number : Nat) : Nat :=
+    (number * (number + 1) / 2) ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    (number * (number + 1) * (2 * number + 1)) / 6
diff --git a/exercises/practice/difference-of-squares/.approaches/recurse-numbers/content.md b/exercises/practice/difference-of-squares/.approaches/recurse-numbers/content.md
new file mode 100644
index 0000000..e2ffce5
--- /dev/null
+++ b/exercises/practice/difference-of-squares/.approaches/recurse-numbers/content.md
@@ -0,0 +1,85 @@
+# Recurse All
+
+In functional languages like Lean, recursion often fills the same role as loops in other languages.
+It is the primary tool used to iterate over a group of elements or a range of values.
+
+This exercise can be solved using straightforward recursion:
+
+```lean
+def sumFirstNPositive (n : Nat) : Nat :=
+    match n with
+    | 0     => 0
+    | x + 1 => (x + 1) + sumFirstNPositive x 
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumFirstNPositive number) ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    match number with
+    | 0     => 0
+    | x + 1 => (x + 1) * (x + 1) + sumOfSquares x
+
+def differenceOfSquares (number : Nat) : Nat :=
+    (squareOfSum number) - (sumOfSquares number)
+```
+
+In cases like this, where a function is defined as a simple pattern match on a value, there is an equivalent and more concise notation:
+
+```lean
+def sumFirstNPositive : Nat -> Nat
+    | 0     => 0
+    | x + 1 => (x + 1) + sumFirstNPositive x 
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumFirstNPositive number) ^ 2
+
+def sumOfSquares : Nat -> Nat
+    | 0     => 0
+    | x + 1 => (x + 1) * (x + 1) + sumOfSquares x
+
+def differenceOfSquares (number : Nat) : Nat :=
+    (squareOfSum number) - (sumOfSquares number)
+```
+
+It is also possible to use `if...then...else` to achieve the same effect:
+
+```lean
+def sumN (n : Nat) :=
+    if n = 0 then 0 else n + sumN (n - 1)
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumN number) ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    if number = 0 then 0 else number ^ 2 + sumOfSquares (number - 1)
+
+def differenceOfSquares (number : Nat) : Nat := (squareOfSum number) - (sumOfSquares number)
+```
+
+Both functions can also be made [tail-recursive][tail-call] by adding an extra accumulating parameter:
+
+```lean
+def sumN (n : Nat) (acc : Nat) : Nat :=
+    if n = 0 then acc else sumN (n - 1) (acc + n)
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumN number 0) ^ 2
+
+def sumSquareN (n : Nat) (acc : Nat) : Nat :=
+    if n = 0 then acc else sumSquareN (n - 1) (acc + (n ^ 2))
+
+def sumOfSquares (number : Nat) : Nat :=
+    sumSquareN number 0
+
+def differenceOfSquares (number : Nat) : Nat := (squareOfSum number) - (sumOfSquares number)
+```
+
+A tail-recursive function may be optimized by the compiler so that it does not require additional stack space, making it as efficient as a loop.
+
+This approach has the advantage of being clear and self-documenting.
+The problem involves summing a range of numbers, and that is exactly what the code expresses.
+
+However, it is also inefficient, since it requires as many recursive calls as `number`, the argument to the functions. 
+Even a tail-recursive variant still requires iterating over all values from `0` up to `number`.
+
+[tail-call]: https://en.wikipedia.org/wiki/Tail_call
diff --git a/exercises/practice/difference-of-squares/.approaches/recurse-numbers/snippet.txt b/exercises/practice/difference-of-squares/.approaches/recurse-numbers/snippet.txt
new file mode 100644
index 0000000..272698b
--- /dev/null
+++ b/exercises/practice/difference-of-squares/.approaches/recurse-numbers/snippet.txt
@@ -0,0 +1,8 @@
+def sumN (n : Nat) (acc : Nat) : Nat :=
+    if n = 0 then acc else sumN (n - 1) (acc + n)
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumN number 0) ^ 2
+
+def sumOfSquares (number : Nat) (acc := 0) : Nat :=
+    if n = 0 then acc else sumSquareN (n - 1) (acc + (n ^ 2))
diff --git a/exercises/practice/difference-of-squares/.articles/config.json b/exercises/practice/difference-of-squares/.articles/config.json
new file mode 100644
index 0000000..4364e86
--- /dev/null
+++ b/exercises/practice/difference-of-squares/.articles/config.json
@@ -0,0 +1,13 @@
+{
+  "articles": [
+    {
+      "uuid": "14152e49-e077-4a8e-a1c2-5812ebb5bbdd",
+      "slug": "formula-is-equivalent-to-recursion",
+      "title": "Proving that the mathematical formula and the recursive approaches are equivalent",
+      "blurb": "proving that the mathematical formula and the recursive approaches are equivalent.",
+      "authors": [
+        "oxe-i"
+      ]
+    }
+  ]
+}
diff --git a/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md b/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md
new file mode 100644
index 0000000..50fd1d4
--- /dev/null
+++ b/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md
@@ -0,0 +1,244 @@
+# Proving the Formula Approach Equivalent to the Recursive Approach
+
+One of Lean's strong points is its integrated proof assistant.
+It empowers the programmer to formally _prove_ properties about the program.
+
+The exercise `difference-of-squares` is well positioned to showcase this feature of the language:
+
+* There is a clear implementation using recursion that directly follows from the problem statement.
+  However, its time complexity is `O(n)`, which makes it relatively slow.
+  This approach is explored in [recurse-numbers][recurse-numbers].
+* On the other hand, there are mathematical formulas that may be used to solve the exercise.
+  They are `O(1)` but result in a less clear implementation that requires previous knowledge.
+  This approach is explored in [mathematical-formula][mathematical-formula].
+
+In particular, whenever there is more than one way to solve a problem, proving that a particular algorithm is equivalent to a reference implementation offers a high degree of trust in its correctness.
+
+Since we are interested in clarity rather than performance, let us consider the direct recursive implementation, without tail recursion.
+It will be our specification:
+
+```lean
+def sumFirstNPositive (n : Nat) : Nat :=
+    match n with
+    | 0     => 0
+    | x + 1 => (x + 1) + sumFirstNPositive x 
+
+def squareOfSum (number : Nat) : Nat :=
+    (sumFirstNPositive number) ^ 2
+
+def sumOfSquares (number : Nat) : Nat :=
+    match number with
+    | 0     => 0
+    | x + 1 => (x + 1) * (x + 1) + sumOfSquares x
+
+def differenceOfSquares (number : Nat) : Nat :=
+    (squareOfSum number) - (sumOfSquares number)
+```
+
+We aim to prove that the following implementation using mathematical formulas is equivalent to our specification using recursion:
+
+```lean
+def sumFirstNPositive' (n : Nat) : Nat :=
+    n * (n + 1) / 2
+
+def squareOfSum' (number : Nat) : Nat :=
+    (sumFirstNPositive number) ^ 2
+
+def sumOfSquares' (number : Nat) : Nat :=
+    (number * (number + 1) * (2 * number + 1)) / 6
+
+def differenceOfSquares' (number : Nat) : Nat :=
+    (squareOfSum number) - (sumOfSquares number)
+```
+
+Note that we have added `'` at the end of those functions to differentiate them from our specification functions.
+
+Since `differenceOfSquares'` and `squareOfSum'` are equal to `differenceOfSquares` and `squareOfSum`, respectively, we need only to prove that `sumFirstNPositive'` is equivalent to `sumFirstNPositive` and that `sumOfSquares'` is equivalent to `sumOfSquares`.
+
+Let us sketch a quick stub for both theorems:
+
+```lean
+theorem sumFirstNPositive_eq_sumFirstNPositive' : sumFirstNPositive = sumFirstNPositive' := by
+    sorry
+
+theorem sumOfSquares_eq_sumOfSquares' : sumOfSquares = sumOfSquares' := by
+    sorry
+```
+
+Note that the proven proposition is the **type** of a value the theorem "returns".
+In Lean, all propositions are types and proofs are values of that type.
+
+The keyword `by` marks the beginning of our proof.
+Right now there is nothing but `sorry`, which is a placeholder used to skip a proof or definition temporarily.
+We must now implement our proof.
+
+There are many ways to prove theorems in Lean.
+Data types such as `Nat` and `List` have rich APIs, full of theorems that can serve as starting points for any proof.
+In addition, Lean provides many [tactics][tactics] that can automate this process.
+
+This is a simple way to prove both theorems, with much of the heavy lifting done by the `simp` and `grind` tactics:
+
+```lean
+theorem sumFirstNPositive_eq_sumFirstNPositive' : sumFirstNPositive = sumFirstNPositive' := by
+    funext n
+    induction n with
+    | zero =>
+      simp [sumFirstNPositive, sumFirstNPositive']
+    | succ x h =>
+      simp [sumFirstNPositive, sumFirstNPositive', h]
+      grind
+
+theorem sumOfSquares_eq_sumOfSquares' : sumOfSquares = sumOfSquares' := by
+    funext n
+    induction n with
+    | zero =>
+      simp [sumOfSquares, sumOfSquares']
+    | succ x h =>
+      simp [sumOfSquares, sumOfSquares', h]
+      grind
+```
+
+Since our theorem proves equality of functions, we start by introducing a variable `n` which is to be applied to both functions.
+This is what `funext n` does.
+The functions will be equivalent if we can prove that, for any value of `n`, their result will be the same.
+
+Since `n` is a `Nat`, which is a nice inductive type, we pattern match on its constructors.
+This is the role of `induction n with`.
+
+There are two possible constructors for a `Nat`: 
+
+1. `zero`, that represents the number `0`, and 
+2. `succ`, which represents the successor of a `Nat` `x`, i.e., `x + 1`.
+
+Once we prove the equivalence holds for `zero`, showing that if it holds for `x`, it also holds for `x + 1`, is enough to prove the equivalence for all `Nat` by induction.
+
+The proof for the case `zero` follows from the simplification of both functions.
+Both `sumFirstNPositive` and `sumOfSquares` are defined to return `0` if their argument is `0`.
+And substituting `0` in the formula for `sumFirstNPositive'` and `sumOfSquares'` will also result in `0`.
+So the equivalence is proved, in both theorems.
+
+In the case of a successor, however, the proof is more involved.
+We leave most of the heavy lifting to `grind`, a powerful tactic that is able to automatically prove many properties involving inequalities, systems of linear equations and other situations.
+
+Note that both theorems use `simp`.
+This tactic tries to simplify a goal, i.e., what we are trying to prove, considering definitions and theorems already proven.
+We use it here to make the definitions of the functions known to the theorem, so that values may be substituted and compared.
+
+It is also possible to prove both theorems from first principles and basic properties and theorems involving `Nat`.
+This is usually a manual task that involves much more work.
+
+The following is an overly verbose proof of `sumFirstNPositive'_eq_sumFirstNPositive` that does not use `grind` or `simp` and relies on basic `Nat` theorems, congruence of functions and sequential calculations of transitive equations:
+
+```lean
+theorem sumFirstNPositive'_eq_sumFirstNPositive (n : Nat) :
+  sumFirstNPositive n = sumFirstNPositive' n := by
+    induction n with
+    | zero      => rfl
+    | succ x h₁ =>
+      have h₂: (x + 1) + x * (x + 1) / 2 = (x + 1) * (x + 2) / 2 := by
+        calc
+          (x + 1) + x * (x + 1) / 2 = 2 * (x + 1) / 2 + x * (x + 1) / 2 := by
+            have h₃: x + 1 = 2 * (x + 1) / 2 := by exact (Nat.mul_div_cancel_left (x + 1) (by decide)).symm
+            exact congrArg (fun t => t + x * (x + 1) / 2) h₃
+          _ = (2 * (x + 1) + x * (x + 1)) / 2 := by
+            have h₃: 2 ∣ 2 * (x + 1) := by
+              exact Nat.dvd_mul_right 2 (x + 1)
+            have h₄: 2 ∣ x * (x + 1) := by
+              have h₅: 2 ∣ x ∨ 2 ∣ (x + 1) := by
+                by_cases h: x % 2 = 0
+                {
+                  left
+                  exact Nat.dvd_iff_mod_eq_zero.mpr h
+                }
+                {
+                  right
+                  have h₆: x % 2 = 1 := by
+                    exact Nat.mod_two_ne_zero.mp h
+                  have h₇: (x + 1) % 2 = 0 := by
+                    calc
+                      (x + 1) % 2 = (x % 2 + 1) % 2 := by
+                        exact Nat.add_mod x 1 2
+                      _ = (1 + 1) % 2 := by
+                        exact congrArg (fun t => (t + 1) % 2) h₆
+                      _ = 0 := by decide
+                  exact Nat.dvd_of_mod_eq_zero h₇
+                }
+              by_cases h: 2 ∣ x
+              {
+                exact Nat.dvd_mul_right_of_dvd h (x + 1)
+              }
+              {
+                have h₆: 2 ∣ (x + 1) := by
+                  exact h₅.resolve_left h
+                exact Nat.dvd_mul_left_of_dvd h₆ x
+              }
+            have h₅: (2 * (x + 1)) % 2 + (x * (x + 1)) % 2 = 0 := by
+              calc
+                (2 * (x + 1)) % 2 + (x * (x + 1)) % 2 = 0 + (x * (x + 1)) % 2 := by
+                  exact congrArg (fun t => t + (x * (x + 1)) % 2) (Nat.mod_eq_zero_of_dvd h₃)
+                _ = 0 := by
+                  exact congrArg (fun t => 0 + t) (Nat.mod_eq_zero_of_dvd h₄)
+            have h₆: ∀ a b c : Nat, c ∣ a → c ∣ b → c > 0 → a / c + b / c = (a + b) / c := by
+              intro a b c h₁ h₂ h₃
+              rcases h₁ with ⟨k, hk⟩
+              rcases h₂ with ⟨l, hl⟩
+              subst hk
+              subst hl
+              calc
+                (c * k) / c + (c * l) / c = (k * c) / c + (c * l) / c := by
+                  exact congrArg (fun t => t / c + (c * l) / c) (Nat.mul_comm c k)
+                _ = (k * c) / c + (l * c) / c := by
+                  exact congrArg (fun t => (k * c) / c + t / c) (Nat.mul_comm c l)
+                _ = k + (l * c) / c := by
+                  exact congrArg (fun t => t + (l * c) / c) (Nat.mul_div_cancel k h₃)
+                _ = k + l := by
+                  exact congrArg (fun t => k + t) (Nat.mul_div_cancel l h₃)
+                _ = (k + l) * c / c := by
+                  exact (Nat.mul_div_cancel (k + l) h₃).symm
+                _ = (k * c + l * c) / c := by
+                  exact congrArg (fun t => t / c) (Nat.add_mul k l c)
+                _ = (c * k + l * c) / c := by
+                  exact congrArg (fun t => (t + l * c) / c) (Nat.mul_comm k c)
+                _ = (c * k + c * l) / c := by
+                  exact congrArg (fun t => (c * k + t) / c) (Nat.mul_comm l c)
+            exact h₆ (2 * (x + 1)) (x * (x + 1)) 2 h₃ h₄ (by decide)
+          _ = ((x + 1) * 2 + x * (x + 1)) / 2 := by
+            exact congrArg (fun t => (t + x * (x + 1)) / 2) (Nat.mul_comm 2 (x + 1))
+          _ = ((x + 1) * 2 + (x + 1) * x) / 2 := by
+            exact congrArg (fun t => ((x + 1) * 2 + t) / 2) (Nat.mul_comm x (x + 1))
+          _ = ((x + 1) * (2 + x)) / 2 := by
+            exact congrArg (fun t => t / 2) (Nat.mul_add (x + 1) 2 x).symm
+          _ = ((x + 1) * (x + 2)) / 2 := by
+            exact congrArg (fun t => ((x + 1) * t) / 2) (Nat.add_comm 2 x)
+      calc
+        sumFirstNPositive (x + 1) = (x + 1) + sumFirstNPositive x := by
+          rfl
+        _ = (x + 1) + x * (x + 1) / 2 := by
+          rw [h₁]
+          rfl
+        _ = (x + 1) * (x + 2) / 2 := by
+          exact h₂
+        _ = sumFirstNPositive' (x + 1) := by
+          rfl
+```
+
+~~~~exercism/note
+We can use the compiler attribute `csimp` on any proof of equivalence between two definitions.
+This attribute instructs the compiler to use the second definition in place of the first:
+
+```lean
+@[csimp]
+theorem sumFirstNPositive_eq_sumFirstNPositive' : sumFirstNPositive = sumFirstNPositive' := by
+    ... -- proof here
+
+-- now any occurrence of `sumFirstNPositive` will be replaced by `sumFirstNPositive'` at runtime.
+```
+
+It is particularly useful in situations where an implementation is more efficient but less clear.
+We can then have a clear specification that is substituted at runtime by the more efficient implementation.
+Many `List` and `Array` functions use this pattern.
+~~~~
+
+[recurse-numbers]: https://exercism.org/tracks/lean/exercises/difference-of-squares/approaches/recurse-numbers
+[mathematical-formula]: https://exercism.org/tracks/lean/exercises/difference-of-squares/approaches/mathematical-formula
+[tactics]: https://lean-lang.org/doc/reference/latest/Tactic-Proofs/#tactics
diff --git a/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/snippet.md b/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/snippet.md
new file mode 100644
index 0000000..dd687f9
--- /dev/null
+++ b/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/snippet.md
@@ -0,0 +1,8 @@
+@[csimp]
+theorem sumFirstNPositive_eq_sumFirstNPositive' : sumFirstNPositive = sumFirstNPositive' := by
+    funext n
+    induction n with
+    | zero => simp [sumFirstNPositive, sumFirstNPositive']
+    | succ x h =>
+      simp [sumFirstNPositive, sumFirstNPositive', h]
+      grind

From 60a9f5b2f053b65f8cc4697305818150eacce747 Mon Sep 17 00:00:00 2001
From: oxe-i <oxe-b@gmail.com>
Date: Sun, 15 Mar 2026 18:52:25 -0300
Subject: [PATCH 2/3] text adjustments in the article

---
 .../content.md                                | 39 +++++++++----------
 .../snippet.md                                |  2 +-
 2 files changed, 20 insertions(+), 21 deletions(-)

diff --git a/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md b/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md
index 50fd1d4..895ab7e 100644
--- a/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md
+++ b/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md
@@ -9,12 +9,12 @@ The exercise `difference-of-squares` is well positioned to showcase this feature
   However, its time complexity is `O(n)`, which makes it relatively slow.
   This approach is explored in [recurse-numbers][recurse-numbers].
 * On the other hand, there are mathematical formulas that may be used to solve the exercise.
-  They are `O(1)` but result in a less clear implementation that requires previous knowledge.
+  They run in `O(1)` time but lead to a less clear implementation that requires prior knowledge.
   This approach is explored in [mathematical-formula][mathematical-formula].
 
-In particular, whenever there is more than one way to solve a problem, proving that a particular algorithm is equivalent to a reference implementation offers a high degree of trust in its correctness.
+In particular, whenever there is more than one way to solve a problem, proving that a particular algorithm is equivalent to a reference implementation offers a high degree of confidence in its correctness.
 
-Since we are interested in clarity rather than performance, let us consider the direct recursive implementation, without tail recursion.
+Since we are interested in clarity rather than performance, we will consider the direct recursive implementation without tail recursion.
 It will be our specification:
 
 ```lean
@@ -42,18 +42,18 @@ def sumFirstNPositive' (n : Nat) : Nat :=
     n * (n + 1) / 2
 
 def squareOfSum' (number : Nat) : Nat :=
-    (sumFirstNPositive number) ^ 2
+    (sumFirstNPositive' number) ^ 2
 
 def sumOfSquares' (number : Nat) : Nat :=
     (number * (number + 1) * (2 * number + 1)) / 6
 
 def differenceOfSquares' (number : Nat) : Nat :=
-    (squareOfSum number) - (sumOfSquares number)
+    (squareOfSum' number) - (sumOfSquares' number)
 ```
 
 Note that we have added `'` at the end of those functions to differentiate them from our specification functions.
 
-Since `differenceOfSquares'` and `squareOfSum'` are equal to `differenceOfSquares` and `squareOfSum`, respectively, we need only to prove that `sumFirstNPositive'` is equivalent to `sumFirstNPositive` and that `sumOfSquares'` is equivalent to `sumOfSquares`.
+Since `differenceOfSquares` and `squareOfSum` are defined in terms of `sumFirstNPositive` and `sumOfSquares`, proving that the formula implementations of these two functions are equivalent is enough to show that the final result is also equivalent.
 
 Let us sketch a quick stub for both theorems:
 
@@ -82,8 +82,7 @@ This is a simple way to prove both theorems, with much of the heavy lifting done
 theorem sumFirstNPositive_eq_sumFirstNPositive' : sumFirstNPositive = sumFirstNPositive' := by
     funext n
     induction n with
-    | zero =>
-      simp [sumFirstNPositive, sumFirstNPositive']
+    | zero => rfl
     | succ x h =>
       simp [sumFirstNPositive, sumFirstNPositive', h]
       grind
@@ -91,18 +90,16 @@ theorem sumFirstNPositive_eq_sumFirstNPositive' : sumFirstNPositive = sumFirstNP
 theorem sumOfSquares_eq_sumOfSquares' : sumOfSquares = sumOfSquares' := by
     funext n
     induction n with
-    | zero =>
-      simp [sumOfSquares, sumOfSquares']
+    | zero => rfl
     | succ x h =>
       simp [sumOfSquares, sumOfSquares', h]
       grind
 ```
 
-Since our theorem proves equality of functions, we start by introducing a variable `n` which is to be applied to both functions.
-This is what `funext n` does.
-The functions will be equivalent if we can prove that, for any value of `n`, their result will be the same.
+Since the theorem states equality between two functions, we first apply _function extensionality_.
+The tactic `funext n` introduces an argument `n` and reduces the goal to proving that both functions return the same value for any `n`.
 
-Since `n` is a `Nat`, which is a nice inductive type, we pattern match on its constructors.
+Since `n` is a `Nat`, which is an inductive type, we proceed by [induction][induction].
 This is the role of `induction n with`.
 
 There are two possible constructors for a `Nat`: 
@@ -112,26 +109,27 @@ There are two possible constructors for a `Nat`:
 
 Once we prove the equivalence holds for `zero`, showing that if it holds for `x`, it also holds for `x + 1`, is enough to prove the equivalence for all `Nat` by induction.
 
-The proof for the case `zero` follows from the simplification of both functions.
+The proof for the case `zero` follows from the substitution of the argument for `0` in both functions.
 Both `sumFirstNPositive` and `sumOfSquares` are defined to return `0` if their argument is `0`.
 And substituting `0` in the formula for `sumFirstNPositive'` and `sumOfSquares'` will also result in `0`.
-So the equivalence is proved, in both theorems.
+So the equivalence is proved, in both theorems, by definitional equality.
+This is what the tactic `rfl` does.
 
 In the case of a successor, however, the proof is more involved.
 We leave most of the heavy lifting to `grind`, a powerful tactic that is able to automatically prove many properties involving inequalities, systems of linear equations and other situations.
 
 Note that both theorems use `simp`.
 This tactic tries to simplify a goal, i.e., what we are trying to prove, considering definitions and theorems already proven.
-We use it here to make the definitions of the functions known to the theorem, so that values may be substituted and compared.
+We use it here to unfold the definitions of the functions, so that values may be substituted and compared.
 
 It is also possible to prove both theorems from first principles and basic properties and theorems involving `Nat`.
 This is usually a manual task that involves much more work.
 
-The following is an overly verbose proof of `sumFirstNPositive'_eq_sumFirstNPositive` that does not use `grind` or `simp` and relies on basic `Nat` theorems, congruence of functions and sequential calculations of transitive equations:
+The following is a much more verbose proof of `sumFirstNPositive_eq_sumFirstNPositive'` that does not use `grind` or `simp` and relies on basic `Nat` theorems, congruence of functions and sequential calculations of transitive equations:
 
 ```lean
-theorem sumFirstNPositive'_eq_sumFirstNPositive (n : Nat) :
-  sumFirstNPositive n = sumFirstNPositive' n := by
+theorem sumFirstNPositive_eq_sumFirstNPositive' : sumFirstNPositive = sumFirstNPositive' := by
+    funext n
     induction n with
     | zero      => rfl
     | succ x h₁ =>
@@ -242,3 +240,4 @@ Many `List` and `Array` functions use this pattern.
 [recurse-numbers]: https://exercism.org/tracks/lean/exercises/difference-of-squares/approaches/recurse-numbers
 [mathematical-formula]: https://exercism.org/tracks/lean/exercises/difference-of-squares/approaches/mathematical-formula
 [tactics]: https://lean-lang.org/doc/reference/latest/Tactic-Proofs/#tactics
+[induction]: https://en.wikipedia.org/wiki/Mathematical_induction
\ No newline at end of file
diff --git a/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/snippet.md b/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/snippet.md
index dd687f9..0780fa4 100644
--- a/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/snippet.md
+++ b/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/snippet.md
@@ -2,7 +2,7 @@
 theorem sumFirstNPositive_eq_sumFirstNPositive' : sumFirstNPositive = sumFirstNPositive' := by
     funext n
     induction n with
-    | zero => simp [sumFirstNPositive, sumFirstNPositive']
+    | zero => rfl
     | succ x h =>
       simp [sumFirstNPositive, sumFirstNPositive', h]
       grind

From 08a671ba5ec53615fd7811d1e63ac540f035f078 Mon Sep 17 00:00:00 2001
From: oxe-i <oxe.github@gmail.com>
Date: Sun, 15 Mar 2026 20:42:24 -0300
Subject: [PATCH 3/3] add eol to article

---
 .../.articles/formula-is-equivalent-to-recursion/content.md     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md b/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md
index 895ab7e..073046c 100644
--- a/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md
+++ b/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md
@@ -240,4 +240,4 @@ Many `List` and `Array` functions use this pattern.
 [recurse-numbers]: https://exercism.org/tracks/lean/exercises/difference-of-squares/approaches/recurse-numbers
 [mathematical-formula]: https://exercism.org/tracks/lean/exercises/difference-of-squares/approaches/mathematical-formula
 [tactics]: https://lean-lang.org/doc/reference/latest/Tactic-Proofs/#tactics
-[induction]: https://en.wikipedia.org/wiki/Mathematical_induction
\ No newline at end of file
+[induction]: https://en.wikipedia.org/wiki/Mathematical_induction