Rewrite ending paragraph of symm breaking section

ITP/symmetry-breaking.tex

@@ -131,14 +131,9 @@
 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.
+Compared to the symmetry-breaking transformation described by Heule and Scheucher,
+our transformation is simpler.
+Nonetheless, proving the above theorem in Lean was tedious,
+as we had to show that the properties from the previous steps were preserved at each new step,
+which carried substantial proof burden.
+In particular, steps 3 through 6 required careful bookkeeping and special handling of the distinguished point~$p_1$.