diff --git a/PhD.lean b/PhD.lean
index c60e64d..e69de29 100644
--- a/PhD.lean
+++ b/PhD.lean
@@ -1 +0,0 @@
-import PhD.RPS.def
diff --git a/blueprint/src/chapter/RPS.tex b/blueprint/src/chapter/RPS.tex
index 17349f2..f1cd4aa 100644
--- a/blueprint/src/chapter/RPS.tex
+++ b/blueprint/src/chapter/RPS.tex
@@ -127,7 +127,7 @@ \section{Additive Group}
   \lean{neg}
   \leanok
   \uses{IsRestricted, isRestricted_iff_abs}
-
+  If $f \in R_c [ \! [ x_1, \dots, x_n ] \! ]$ then $-f \in R_c [ \! [ x_1, \dots, x_n ] \! ]$.
 \end{lemma}
 
 \begin{proof}