diff --git a/common/Common/Data/Real/Geometry.lean b/common/Common/Data/Real/Geometry.lean
index bd54511..1eb8d8c 100644
--- a/common/Common/Data/Real/Geometry.lean
+++ b/common/Common/Data/Real/Geometry.lean
@@ -1,27 +1,2 @@
-import Mathlib.Data.Real.Sqrt
-import Mathlib.Logic.Function.Basic
-
-namespace Real
-
-notation "ℝ²" => ℝ × ℝ
-
-noncomputable def dist (x y : ℝ²) :=
-  Real.sqrt ((abs (y.1 - x.1)) ^ 2 + (abs (y.2 - x.2)) ^ 2)
-
-def similar (S T : Set ℝ²) : Prop :=
-  ∃ f : ℝ² → ℝ², Function.Bijective f ∧
-    ∃ s : ℝ, ∀ x y : ℝ², x ∈ S ∧ y ∈ T →
-      s * dist x y = dist (f x) (f y)
-
-def congruent (S T : Set (ℝ × ℝ)) : Prop :=
-  ∃ f : ℝ² → ℝ², Function.Bijective f ∧
-    ∀ x y : ℝ², x ∈ S ∧ y ∈ T →
-      dist x y = dist (f x) (f y)
-
-theorem congruent_similar {S T : Set ℝ²} : congruent S T → similar S T := by
-  intro hc
-  let ⟨f, ⟨hf, hs⟩⟩ := hc
-  conv at hs => intro x y hxy; arg 1; rw [← one_mul (dist x y)]
-  exact ⟨f, ⟨hf, ⟨1, hs⟩⟩⟩
-
-end Real
\ No newline at end of file
+import Common.Data.Real.Geometry.Basic
+import Common.Data.Real.Geometry.Rectangle
\ No newline at end of file
diff --git a/common/Common/Data/Real/Geometry/Basic.lean b/common/Common/Data/Real/Geometry/Basic.lean
new file mode 100644
index 0000000..b6756d6
--- /dev/null
+++ b/common/Common/Data/Real/Geometry/Basic.lean
@@ -0,0 +1,41 @@
+import Mathlib.Data.Real.Sqrt
+
+notation "ℝ²" => ℝ × ℝ
+
+namespace Real
+
+/--
+Determine the distance between two points in `ℝ²`.
+-/
+noncomputable def dist (x y : ℝ²) :=
+  Real.sqrt ((abs (y.1 - x.1)) ^ 2 + (abs (y.2 - x.2)) ^ 2)
+
+/--
+Two sets `S` and `T` are `similar` iff there exists a one-to-one correspondence
+between `S` and `T` such that the distance between any two points `P, Q ∈ S` and
+corresponding points `P', Q' ∈ T` differ by some constant `α`. In other words,
+`α|PQ| = |P'Q'|`.
+-/
+def similar (S T : Set ℝ²) : Prop :=
+  ∃ f : ℝ² → ℝ², Function.Bijective f ∧
+    ∃ s : ℝ, ∀ x y : ℝ², x ∈ S ∧ y ∈ T →
+      s * dist x y = dist (f x) (f y)
+
+/--
+Two sets are congruent if they are similar with a scaling factor of `1`.
+-/
+def congruent (S T : Set (ℝ × ℝ)) : Prop :=
+  ∃ f : ℝ² → ℝ², Function.Bijective f ∧
+    ∀ x y : ℝ², x ∈ S ∧ y ∈ T →
+      dist x y = dist (f x) (f y)
+
+/--
+Any two congruent sets must be similar to one another.
+-/
+theorem congruent_similar {S T : Set ℝ²} : congruent S T → similar S T := by
+  intro hc
+  let ⟨f, ⟨hf, hs⟩⟩ := hc
+  conv at hs => intro x y hxy; arg 1; rw [← one_mul (dist x y)]
+  exact ⟨f, ⟨hf, ⟨1, hs⟩⟩⟩
+
+end Real
\ No newline at end of file
diff --git a/common/Common/Data/Real/Geometry/Rectangle.lean b/common/Common/Data/Real/Geometry/Rectangle.lean
new file mode 100644
index 0000000..ac754fc
--- /dev/null
+++ b/common/Common/Data/Real/Geometry/Rectangle.lean
@@ -0,0 +1,39 @@
+import Common.Data.Real.Geometry.Basic
+
+namespace Real
+
+/--
+A `Rectangle` is characterized by two points defining opposite corners. We
+arbitrarily choose the bottom left and top right points to perform this
+characterization.
+-/
+structure Rectangle (bottom_left : ℝ²) (top_right : ℝ²)
+
+namespace Rectangle
+
+/--
+A `Rectangle` is the locus of points making up its edges.
+-/
+def set_eq (r : Rectangle x y) : Set ℝ² := sorry
+
+/--
+Computes the bottom right corner of a `Rectangle`.
+-/
+def bottom_right (r : Rectangle x y) : ℝ² := sorry
+
+/--
+Computes the top left corner of a `Rectangle`.
+-/
+def top_left (r : Rectangle x y) : ℝ² := sorry
+
+/--
+Computes the width of a `Rectangle`.
+-/
+def width (r : Rectangle x y) : ℝ := sorry
+
+/--
+Computes the height of a `Rectangle`.
+-/
+def height (r : Rectangle x y) : ℝ := sorry
+
+end Real.Rectangle
\ No newline at end of file
diff --git a/common/Common/Data/Real/Sequence.lean b/common/Common/Data/Real/Sequence.lean
index 6500bea..1b0cdf5 100644
--- a/common/Common/Data/Real/Sequence.lean
+++ b/common/Common/Data/Real/Sequence.lean
@@ -1,206 +1,2 @@
-import Mathlib.Data.Real.Basic
-import Mathlib.Tactic.NormNum
-import Mathlib.Tactic.Ring
-
-/--
-A `0`th-indexed arithmetic sequence.
--/
-structure Arithmetic where
-  a₀ : Real
-  Δ : Real
-
-namespace Arithmetic
-
-/--
-Returns the value of the `n`th term of an arithmetic sequence.
-
-This function calculates the value of this term directly. Keep in mind the
-sequence is `0`th-indexed.
--/
-def termClosed (seq : Arithmetic) (n : Nat) : Real :=
-  seq.a₀ + seq.Δ * n
-
-/--
-Returns the value of the `n`th term of an arithmetic sequence.
-
-This function calculates the value of this term recursively. Keep in mind the
-sequence is `0`th-indexed.
--/
-def termRecursive : Arithmetic → Nat → Real
-  | seq,       0 => seq.a₀
-  | seq, (n + 1) => seq.Δ + seq.termRecursive n
-
-/--
-The recursive and closed term definitions of an arithmetic sequence agree with
-one another.
--/
-theorem term_recursive_closed (seq : Arithmetic) (n : Nat)
-  : seq.termRecursive n = seq.termClosed n := by
-  induction n with
-  | zero => unfold termRecursive termClosed; norm_num
-  | succ n ih =>
-    calc
-      termRecursive seq (Nat.succ n)
-      _ = seq.Δ + seq.termRecursive n := rfl
-      _ = seq.Δ + seq.termClosed n := by rw [ih]
-      _ = seq.Δ + (seq.a₀ + seq.Δ * n) := rfl
-      _ = seq.a₀ + seq.Δ * (↑n + 1) := by ring
-      _ = seq.a₀ + seq.Δ * ↑(n + 1) := by simp
-      _ = termClosed seq (n + 1) := rfl
-
-/--
-A term is equal to the next in the sequence minus the common difference.
--/
-theorem term_closed_sub_succ_delta {seq : Arithmetic}
-  : seq.termClosed n = seq.termClosed (n + 1) - seq.Δ :=
-  calc
-    seq.termClosed n
-    _ = seq.a₀ + seq.Δ * n := rfl
-    _ = seq.a₀ + seq.Δ * n + seq.Δ - seq.Δ := by rw [add_sub_cancel]
-    _ = seq.a₀ + seq.Δ * (↑n + 1) - seq.Δ := by ring_nf
-    _ = seq.a₀ + seq.Δ * ↑(n + 1) - seq.Δ := by simp only [Nat.cast_add, Nat.cast_one]
-    _ = seq.termClosed (n + 1) - seq.Δ := rfl
-
-/--
-The summation of the first `n + 1` terms of an arithmetic sequence.
-
-This function calculates the sum directly.
--/
-noncomputable def sum_closed (seq : Arithmetic) (n : Nat) : Real :=
-  (n + 1) * (seq.a₀ + seq.termClosed n) / 2
-
-/--
-The summation of the first `n + 1` terms of an arithmetic sequence.
-
-This function calculates the sum recursively.
--/
-def sum_recursive : Arithmetic → Nat → Real
-  | seq,       0 => seq.a₀
-  | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n
-
-/--
-Simplify a summation of terms found in the proof of `sum_recursive_closed`.
--/
-private lemma sub_delta_summand_eq_two_mul_a₀ {seq : Arithmetic}
-  : seq.a₀ + seq.termClosed (n + 1) - (n + 1) * seq.Δ = 2 * seq.a₀ :=
-  calc
-    seq.a₀ + seq.termClosed (n + 1) - (n + 1) * seq.Δ
-    _ = seq.a₀ + (seq.a₀ + seq.Δ * ↑(n + 1)) - (n + 1) * seq.Δ := rfl
-    _ = seq.a₀ + seq.a₀ + seq.Δ * ↑(n + 1) - (n + 1) * seq.Δ := by rw [←add_assoc]
-    _ = seq.a₀ + seq.a₀ + seq.Δ * (n + 1) - (n + 1) * seq.Δ := by simp only [Nat.cast_add, Nat.cast_one]
-    _ = 2 * seq.a₀ := by ring_nf
-
-/--
-The recursive and closed definitions of the sum of an arithmetic sequence agree
-with one another.
--/
-theorem sum_recursive_closed (seq : Arithmetic) (n : Nat)
-  : seq.sum_recursive n = seq.sum_closed n := by
-  induction n with
-  | zero =>
-    unfold sum_recursive sum_closed termClosed
-    norm_num
-  | succ n ih =>
-    calc
-      seq.sum_recursive (n + 1)
-      _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl
-      _ = seq.termClosed (n + 1) + seq.sum_closed n := by rw [ih]
-      _ = seq.termClosed (n + 1) + ((n + 1) * (seq.a₀ + seq.termClosed n)) / 2 := rfl
-      _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed n + seq.a₀ + seq.termClosed n) / 2 := by ring_nf
-      _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * (seq.termClosed (n + 1) - seq.Δ) + seq.a₀ + (seq.termClosed (n + 1) - seq.Δ)) / 2 := by rw [@term_closed_sub_succ_delta n]
-      _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed (n + 1) + (seq.a₀ + seq.termClosed (n + 1) - (n + 1) * seq.Δ)) / 2 := by ring_nf
-      _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed (n + 1) + 2 * seq.a₀) / 2 := by rw [sub_delta_summand_eq_two_mul_a₀]
-      _ = ((n + 1) + 1) * (seq.a₀ + seq.termClosed (n + 1)) / 2 := by ring_nf
-      _ = (↑(n + 1) + 1) * (seq.a₀ + seq.termClosed (n + 1)) / 2 := by simp only [Nat.cast_add, Nat.cast_one]
-      _ = seq.sum_closed (n + 1) := rfl
-
-end Arithmetic
-
-/--
-A `0th`-indexed geometric sequence.
--/
-structure Geometric where
-  a₀ : Real
-  r : Real
-
-namespace Geometric
-
-/--
-Returns the value of the `n`th term of a geometric sequence.
-
-This function calculates the value of this term directly. Keep in mind the
-sequence is `0`th-indexed.
--/
-def termClosed (seq : Geometric) (n : Nat) : Real :=
-  seq.a₀ * seq.r ^ n
-
-/--
-Returns the value of the `n`th term of a geometric sequence.
-
-This function calculates the value of this term recursively. Keep in mind the
-sequence is `0`th-indexed.
--/
-def termRecursive : Geometric → Nat → Real
-  | seq,       0 => seq.a₀
-  | seq, (n + 1) => seq.r * (seq.termRecursive n)
-
-/--
-The recursive and closed term definitions of a geometric sequence agree with
-one another.
--/
-theorem term_recursive_closed (seq : Geometric) (n : Nat)
-  : seq.termRecursive n = seq.termClosed n := by
-  induction n with
-  | zero => unfold termClosed termRecursive; norm_num
-  | succ n ih => calc
-      seq.termRecursive (n + 1)
-      _ = seq.r * (seq.termRecursive n) := rfl
-      _ = seq.r * (seq.termClosed n) := by rw [ih]
-      _ = seq.r * (seq.a₀ * seq.r ^ n) := rfl
-      _ = seq.a₀ * seq.r ^ (n + 1) := by ring
-      _ = seq.termClosed (n + 1) := rfl
-
-/--
-The summation of the first `n + 1` terms of a geometric sequence.
-
-This function calculates the sum directly.
--/
-noncomputable def sum_closed_ratio_neq_one (seq : Geometric) (n : Nat)
-  : seq.r ≠ 1 → Real :=
-  fun _ => (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r)
-
-/--
-The summation of the first `n + 1` terms of a geometric sequence.
-
-This function calculates the sum recursively.
--/
-def sum_recursive : Geometric → Nat → Real
-  | seq,       0 => seq.a₀
-  | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n
-
-/--
-The recursive and closed definitions of the sum of a geometric sequence agree
-with one another.
--/
-theorem sum_recursive_closed (seq : Geometric) (n : Nat) (p : seq.r ≠ 1)
-  : sum_recursive seq n = sum_closed_ratio_neq_one seq n p := by
-  have h : 1 - seq.r ≠ 0 := by
-    intro h
-    rw [sub_eq_iff_eq_add, zero_add] at h
-    exact False.elim (p (Eq.symm h))
-  induction n with
-  | zero =>
-    unfold sum_recursive sum_closed_ratio_neq_one
-    simp
-    rw [mul_div_assoc, div_self h, mul_one] 
-  | succ n ih =>
-    calc
-      sum_recursive seq (n + 1)
-      _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl
-      _ = seq.termClosed (n + 1) + sum_closed_ratio_neq_one seq n p := by rw [ih]
-      _ = seq.a₀ * seq.r ^ (n + 1) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := rfl
-      _ = seq.a₀ * seq.r ^ (n + 1) * (1 - seq.r) / (1 - seq.r) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := by rw [mul_div_cancel _ h]
-      _ = (seq.a₀ * (1 - seq.r ^ (n + 1 + 1))) / (1 - seq.r) := by ring_nf
-      _ = sum_closed_ratio_neq_one seq (n + 1) p := rfl
-
-end Geometric
+import Common.Data.Real.Sequence.Arithmetic
+import Common.Data.Real.Sequence.Geometric
\ No newline at end of file
diff --git a/common/Common/Data/Real/Sequence/Arithmetic.lean b/common/Common/Data/Real/Sequence/Arithmetic.lean
new file mode 100644
index 0000000..a334d20
--- /dev/null
+++ b/common/Common/Data/Real/Sequence/Arithmetic.lean
@@ -0,0 +1,117 @@
+import Mathlib.Data.Real.Basic
+
+namespace Real
+
+/--
+A `0`th-indexed arithmetic sequence.
+-/
+structure Arithmetic where
+  a₀ : Real
+  Δ : Real
+
+namespace Arithmetic
+
+/--
+Returns the value of the `n`th term of an arithmetic sequence.
+
+This function calculates the value of this term directly. Keep in mind the
+sequence is `0`th-indexed.
+-/
+def termClosed (seq : Arithmetic) (n : Nat) : Real :=
+  seq.a₀ + seq.Δ * n
+
+/--
+Returns the value of the `n`th term of an arithmetic sequence.
+
+This function calculates the value of this term recursively. Keep in mind the
+sequence is `0`th-indexed.
+-/
+def termRecursive : Arithmetic → Nat → Real
+  | seq,       0 => seq.a₀
+  | seq, (n + 1) => seq.Δ + seq.termRecursive n
+
+/--
+The recursive and closed term definitions of an arithmetic sequence agree with
+one another.
+-/
+theorem term_recursive_closed (seq : Arithmetic) (n : Nat)
+  : seq.termRecursive n = seq.termClosed n := by
+  induction n with
+  | zero => unfold termRecursive termClosed; norm_num
+  | succ n ih =>
+    calc
+      termRecursive seq (Nat.succ n)
+      _ = seq.Δ + seq.termRecursive n := rfl
+      _ = seq.Δ + seq.termClosed n := by rw [ih]
+      _ = seq.Δ + (seq.a₀ + seq.Δ * n) := rfl
+      _ = seq.a₀ + seq.Δ * (↑n + 1) := by ring
+      _ = seq.a₀ + seq.Δ * ↑(n + 1) := by simp
+      _ = termClosed seq (n + 1) := rfl
+
+/--
+A term is equal to the next in the sequence minus the common difference.
+-/
+theorem term_closed_sub_succ_delta {seq : Arithmetic}
+  : seq.termClosed n = seq.termClosed (n + 1) - seq.Δ :=
+  calc
+    seq.termClosed n
+    _ = seq.a₀ + seq.Δ * n := rfl
+    _ = seq.a₀ + seq.Δ * n + seq.Δ - seq.Δ := by rw [add_sub_cancel]
+    _ = seq.a₀ + seq.Δ * (↑n + 1) - seq.Δ := by ring_nf
+    _ = seq.a₀ + seq.Δ * ↑(n + 1) - seq.Δ := by simp only [Nat.cast_add, Nat.cast_one]
+    _ = seq.termClosed (n + 1) - seq.Δ := rfl
+
+/--
+The summation of the first `n + 1` terms of an arithmetic sequence.
+
+This function calculates the sum directly.
+-/
+noncomputable def sum_closed (seq : Arithmetic) (n : Nat) : Real :=
+  (n + 1) * (seq.a₀ + seq.termClosed n) / 2
+
+/--
+The summation of the first `n + 1` terms of an arithmetic sequence.
+
+This function calculates the sum recursively.
+-/
+def sum_recursive : Arithmetic → Nat → Real
+  | seq,       0 => seq.a₀
+  | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n
+
+/--
+Simplify a summation of terms found in the proof of `sum_recursive_closed`.
+-/
+private lemma sub_delta_summand_eq_two_mul_a₀ {seq : Arithmetic}
+  : seq.a₀ + seq.termClosed (n + 1) - (n + 1) * seq.Δ = 2 * seq.a₀ :=
+  calc
+    seq.a₀ + seq.termClosed (n + 1) - (n + 1) * seq.Δ
+    _ = seq.a₀ + (seq.a₀ + seq.Δ * ↑(n + 1)) - (n + 1) * seq.Δ := rfl
+    _ = seq.a₀ + seq.a₀ + seq.Δ * ↑(n + 1) - (n + 1) * seq.Δ := by rw [←add_assoc]
+    _ = seq.a₀ + seq.a₀ + seq.Δ * (n + 1) - (n + 1) * seq.Δ := by simp only [Nat.cast_add, Nat.cast_one]
+    _ = 2 * seq.a₀ := by ring_nf
+
+/--
+The recursive and closed definitions of the sum of an arithmetic sequence agree
+with one another.
+-/
+theorem sum_recursive_closed (seq : Arithmetic) (n : Nat)
+  : seq.sum_recursive n = seq.sum_closed n := by
+  induction n with
+  | zero =>
+    unfold sum_recursive sum_closed termClosed
+    norm_num
+  | succ n ih =>
+    calc
+      seq.sum_recursive (n + 1)
+      _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl
+      _ = seq.termClosed (n + 1) + seq.sum_closed n := by rw [ih]
+      _ = seq.termClosed (n + 1) + ((n + 1) * (seq.a₀ + seq.termClosed n)) / 2 := rfl
+      _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed n + seq.a₀ + seq.termClosed n) / 2 := by ring_nf
+      _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * (seq.termClosed (n + 1) - seq.Δ) + seq.a₀ + (seq.termClosed (n + 1) - seq.Δ)) / 2 := by rw [@term_closed_sub_succ_delta n]
+      _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed (n + 1) + (seq.a₀ + seq.termClosed (n + 1) - (n + 1) * seq.Δ)) / 2 := by ring_nf
+      _ = (2 * seq.termClosed (n + 1) + n * seq.a₀ + n * seq.termClosed (n + 1) + 2 * seq.a₀) / 2 := by rw [sub_delta_summand_eq_two_mul_a₀]
+      _ = ((n + 1) + 1) * (seq.a₀ + seq.termClosed (n + 1)) / 2 := by ring_nf
+      _ = (↑(n + 1) + 1) * (seq.a₀ + seq.termClosed (n + 1)) / 2 := by simp only [Nat.cast_add, Nat.cast_one]
+      _ = seq.sum_closed (n + 1) := rfl
+
+end Real.Arithmetic
\ No newline at end of file
diff --git a/common/Common/Data/Real/Sequence/Geometric.lean b/common/Common/Data/Real/Sequence/Geometric.lean
new file mode 100644
index 0000000..31da033
--- /dev/null
+++ b/common/Common/Data/Real/Sequence/Geometric.lean
@@ -0,0 +1,92 @@
+import Mathlib.Data.Real.Basic
+
+namespace Real
+
+/--
+A `0th`-indexed geometric sequence.
+-/
+structure Geometric where
+  a₀ : Real
+  r : Real
+
+namespace Geometric
+
+/--
+Returns the value of the `n`th term of a geometric sequence.
+
+This function calculates the value of this term directly. Keep in mind the
+sequence is `0`th-indexed.
+-/
+def termClosed (seq : Geometric) (n : Nat) : Real :=
+  seq.a₀ * seq.r ^ n
+
+/--
+Returns the value of the `n`th term of a geometric sequence.
+
+This function calculates the value of this term recursively. Keep in mind the
+sequence is `0`th-indexed.
+-/
+def termRecursive : Geometric → Nat → Real
+  | seq,       0 => seq.a₀
+  | seq, (n + 1) => seq.r * (seq.termRecursive n)
+
+/--
+The recursive and closed term definitions of a geometric sequence agree with
+one another.
+-/
+theorem term_recursive_closed (seq : Geometric) (n : Nat)
+  : seq.termRecursive n = seq.termClosed n := by
+  induction n with
+  | zero => unfold termClosed termRecursive; norm_num
+  | succ n ih => calc
+      seq.termRecursive (n + 1)
+      _ = seq.r * (seq.termRecursive n) := rfl
+      _ = seq.r * (seq.termClosed n) := by rw [ih]
+      _ = seq.r * (seq.a₀ * seq.r ^ n) := rfl
+      _ = seq.a₀ * seq.r ^ (n + 1) := by ring
+      _ = seq.termClosed (n + 1) := rfl
+
+/--
+The summation of the first `n + 1` terms of a geometric sequence.
+
+This function calculates the sum directly.
+-/
+noncomputable def sum_closed_ratio_neq_one (seq : Geometric) (n : Nat)
+  : seq.r ≠ 1 → Real :=
+  fun _ => (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r)
+
+/--
+The summation of the first `n + 1` terms of a geometric sequence.
+
+This function calculates the sum recursively.
+-/
+def sum_recursive : Geometric → Nat → Real
+  | seq,       0 => seq.a₀
+  | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n
+
+/--
+The recursive and closed definitions of the sum of a geometric sequence agree
+with one another.
+-/
+theorem sum_recursive_closed (seq : Geometric) (n : Nat) (p : seq.r ≠ 1)
+  : sum_recursive seq n = sum_closed_ratio_neq_one seq n p := by
+  have h : 1 - seq.r ≠ 0 := by
+    intro h
+    rw [sub_eq_iff_eq_add, zero_add] at h
+    exact False.elim (p (Eq.symm h))
+  induction n with
+  | zero =>
+    unfold sum_recursive sum_closed_ratio_neq_one
+    simp
+    rw [mul_div_assoc, div_self h, mul_one] 
+  | succ n ih =>
+    calc
+      sum_recursive seq (n + 1)
+      _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl
+      _ = seq.termClosed (n + 1) + sum_closed_ratio_neq_one seq n p := by rw [ih]
+      _ = seq.a₀ * seq.r ^ (n + 1) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := rfl
+      _ = seq.a₀ * seq.r ^ (n + 1) * (1 - seq.r) / (1 - seq.r) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := by rw [mul_div_cancel _ h]
+      _ = (seq.a₀ * (1 - seq.r ^ (n + 1 + 1))) / (1 - seq.r) := by ring_nf
+      _ = sum_closed_ratio_neq_one seq (n + 1) p := rfl
+
+end Real.Geometric
\ No newline at end of file