diff --git a/FormalBook/Chapter_02.lean b/FormalBook/Chapter_02.lean
index 5531b26..810595b 100644
--- a/FormalBook/Chapter_02.lean
+++ b/FormalBook/Chapter_02.lean
@@ -15,7 +15,6 @@ limitations under the License.
 
 Authors: Moritz Firsching
 -/
-import Mathlib.Algebra.Lie.OfAssociative
 import Mathlib.Analysis.Convex.SpecificFunctions.Basic
 import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
 import Mathlib.Data.Nat.Choose.Factorization
@@ -38,7 +37,7 @@ formalized by Patrick Stevens and Bolton Bailey.
 -/
 open scoped BigOperators
 
-namespace chapter02
+namespace chapter2
 
 open Real
 
@@ -226,4 +225,4 @@ theorem exists_prime_lt_and_le_two_mul (n : ℕ) (hn0 : n ≠ 0) :
 
 
 
-end chapter02
+end chapter2
diff --git a/blueprint/src/chapter/chapter02.tex b/blueprint/src/chapter/chapter02.tex
index c90eda7..cede05b 100644
--- a/blueprint/src/chapter/chapter02.tex
+++ b/blueprint/src/chapter/chapter02.tex
@@ -1 +1,13 @@
 \chapter{Bertrand's postulate}
+
+\begin{theorem}
+    \label{thm:bertrands_postulate}
+    \lean{chapter2.exists_prime_lt_and_le_two_mul}
+    \leanok
+    For any positive natural number, there is a prime which is greater than
+    it, but no more than twice as large.
+\end{theorem}
+\begin{proof}
+    \leanok
+    TODO: make this follow the book proof more closely!
+\end{proof}
\ No newline at end of file