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..073046c
--- /dev/null
+++ b/exercises/practice/difference-of-squares/.articles/formula-is-equivalent-to-recursion/content.md
@@ -0,0 +1,243 @@
+# 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 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 confidence in its correctness.
+
+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
+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 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:
+
+```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 => rfl
+    | succ x h =>
+      simp [sumFirstNPositive, sumFirstNPositive', h]
+      grind
+
+theorem sumOfSquares_eq_sumOfSquares' : sumOfSquares = sumOfSquares' := by
+    funext n
+    induction n with
+    | zero => rfl
+    | succ x h =>
+      simp [sumOfSquares, sumOfSquares', h]
+      grind
+```
+
+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 an inductive type, we proceed by [induction][induction].
+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 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, 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 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 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' : sumFirstNPositive = sumFirstNPositive' := by
+    funext n
+    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
+[induction]: https://en.wikipedia.org/wiki/Mathematical_induction
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..0780fa4
--- /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 => rfl
+    | succ x h =>
+      simp [sumFirstNPositive, sumFirstNPositive', h]
+      grind