Fiddling with the discussion of the various ladders in chapter 5.

paper/5_highlevel.tex

@@ -276,7 +276,8 @@ we define a ladder \coqe{opt_montgomery} (in which $\K$ has not been fixed yet),
 similar to the one used in
 TweetNaCl.
 (This definition is closely related to \coqe{montgomery_rec} that was used
-in the definition of \coqe{RFC}, and is easily proved the same.)
+in the definition of \coqe{RFC}, and is easily proved to correspond to it.
+In Coq this correspondence proof is hidden in the proof of \coqe{RFC_Correct} shown above.)
 %\ref to the def of montgomery_rec? relevant lemma(s) that show(s) these are "the same"?
 
 We prove its correctness for any points which \xcoord is not 0.