feat> 2025 day 9 part 1

.src/2025_desc.txt

@@ -123,3 +123,17 @@ Now, we should add all edges, from the shortest to the largest, until the graph
 connected component.
 Once that happens, we should report the product of the `x`-coordinates of the last edge that was
 added.
+-- Day 9
+The input are the coordinates of the red tiles.
+
+### Description
+
+#### Part 1
+
+In part 1, we should determine the largest area of a rectangle with two opposite corners
+on the red tiles.
+
+#### Part 2
+
+In part 2, we should still find the largest rectangle with opposite vertices on the red tiles,
+but the rectangle must be entirely contained in the interior of the path.

.src/todo.md

@@ -38,3 +38,4 @@
 
 ### 2025
 * Day 8: both parts are slow, the first one is only sped up by a hard-coded answer.
+* Day 9, part 2: missing -- finding rectangles in the interior of a region.

Advents.lean

@@ -7,3 +7,4 @@ import Advents.AoC2025.day05
 import Advents.AoC2025.day06
 import Advents.AoC2025.day07
 import Advents.AoC2025.day08
+import Advents.AoC2025.day09

Advents/AoC2025/2025_descriptions.md

@@ -8,3 +8,4 @@
 | [6](2025_descriptions_with_tests.md#day-6) | Helping cephalopods with their maths homework                                                       |
 | [7](2025_descriptions_with_tests.md#day-7) | Splitting tachyon manifolds                                                                         |
 | [8](2025_descriptions_with_tests.md#day-8) | Powering up Christmas decorations                                                                   |
+| [9](2025_descriptions_with_tests.md#day-9) | The input are the coordinates of the red tiles.                                                     |

Advents/AoC2025/2025_descriptions_with_tests.md

@@ -287,3 +287,36 @@ added.
 [Solution in Lean](day08.lean)
 
 ---
+
+#  [Day 9](https://adventofcode.com/2025/day/9)
+
+The input are the coordinates of the red tiles.
+
+####  Test
+
+<pre>
+7,1
+11,1
+11,7
+9,7
+9,5
+2,5
+2,3
+7,3
+</pre>
+
+### Description
+
+#### Part 1
+
+In part 1, we should determine the largest area of a rectangle with two opposite corners
+on the red tiles.
+
+#### Part 2
+
+In part 2, we should still find the largest rectangle with opposite vertices on the red tiles,
+but the rectangle must be entirely contained in the interior of the path.
+
+[Solution in Lean](day09.lean)
+
+---