diff --git a/protocol/protocol.tex b/protocol/protocol.tex
index 87d8657e..76817a1b 100644
--- a/protocol/protocol.tex
+++ b/protocol/protocol.tex
@@ -9785,7 +9785,9 @@ Peter Newell's illustration of the Jubjub bird, from \cite{Carroll1902}.
           Edwards curves $\Edwards{a,d}$, Montgomery curves $\Montgomery{A,B}$, and
           extractors $\Extractor{\Adversary}$.
     \item Correct a use of $\GroupJ$ that should have been $\MontCurve$ in the proof of
-          \theoremref{thmdistinctxcriterion}.
+          \theoremref{thmdistinctxcriterion}, and make a minor tweak to the theorem statement
+          ($k_2 \neq \pm k_1$ instead of $k_1 \neq \pm k_2$) to make the contradiction
+          derived by the proof clearer.
     \item Address some of the findings of the QED-it report:
           \begin{itemize}
             \item Improved cross-referencing in \crossref{concretepedersenhash}.
@@ -11314,7 +11316,7 @@ Let $Q$ be a point of odd-prime order $s$ on a Montgomery curve
 $\MontCurve = \Montgomery{\ParamM{A},\ParamM{B}}$ over $\GF{\ParamS{r}}$.
 Let $k_\barerange{1}{2}$ be integers in $\bigrangenozero{-\halfs}{\halfs}$.
 Let $P_i = \scalarmult{k_i}{Q} = (x_i, y_i)$ for $i \in \range{1}{2}$, with
-$k_1 \neq \pm k_2$. Then the non-unified addition constraints
+$k_2 \neq \pm k_1$. Then the non-unified addition constraints
 
 \begin{formulae}
   \item $\constraint{x_2 - x_1}{\lambda}{y_2 - y_1}$
@@ -11342,8 +11344,8 @@ then $k_2 = \pm k_1$ (contradiction).
 The conditions of this theorem are called the \distinctXCriterion.
 
 In particular, if $k_\barerange{1}{2}$ are integers in $\bigrange{1}{\halfs}$
-then it is sufficient to require $k_1 \neq k_2$, since that implies
-$k_1 \neq \pm k_2$.
+then it is sufficient to require $k_2 \neq k_1$, since that implies
+$k_2 \neq \pm k_1$.
 
 \vspace{2ex}
 \introlist