diff --git a/LeanTalkSP24.lean b/LeanTalkSP24.lean
index 870a651..c7928f8 100644
--- a/LeanTalkSP24.lean
+++ b/LeanTalkSP24.lean
@@ -1,5 +1,6 @@
 -- This module serves as the root of the `«LeanTalkSP24»` library.
 -- Import modules here that should be built as part of the library.
 import «LeanTalkSP24».basics
+import «LeanTalkSP24».basics2
 import «LeanTalkSP24».infinitely_many_primes
 import «LeanTalkSP24».polynomial_over_field_dim_one
diff --git a/LeanTalkSP24/basics2.lean b/LeanTalkSP24/basics2.lean
new file mode 100644
index 0000000..307fa2f
--- /dev/null
+++ b/LeanTalkSP24/basics2.lean
@@ -0,0 +1,20 @@
+import Mathlib.Tactic
+
+open Finset
+
+theorem sum_first_n {n : ℕ} : 2 * (range (n + 1)).sum id = n * (n + 1) := by
+  induction' n with d hd
+  · simp
+  · rw [sum_range_succ, mul_add, hd, id.def, Nat.succ_eq_add_one]
+    linarith
+
+open Set
+variable {α : Type _}
+variable {s t u : Set α}
+
+example : s ∪ s ∩ t = s := by
+  ext x; constructor
+  rintro (xs | xsti)
+  · trivial
+  · exact And.left xsti
+  exact Or.inl