diff --git a/ITP/symmetry-breaking.tex b/ITP/symmetry-breaking.tex
index 3f4e757..0f2dd16 100644
--- a/ITP/symmetry-breaking.tex
+++ b/ITP/symmetry-breaking.tex
@@ -130,3 +130,15 @@
 \end{align*}
 This concludes the proof.
 \end{proof}
+
+We had quite some difficulty formalizing the symmetry-breaking argument.
+We spent many hours around a whiteboard,
+simplifying the argument to minimize the amount of theory we would need to develop.
+The projective transformation in Step 3 was particularly difficult to wrangle.
+This step, and those after it, requires careful bookkeeping around the distinguished point $p_1$.
+
+Once these details were worked out,
+the proof was relatively straightforward, albeit long and tedious.
+Each step of the proof justifies not only that a new property is achieved,
+but also that all properties from previous steps are preserved.
+As a result, the proof burden was substantial.