Simplifications for Theorem 11.2.12 {RD-cauchy-complete}

[lowasser]

While implementing this result in agda-unimath (UniMath/agda-unimath#1343), I came across a few simplifications to the current proof. I'll go in order of the things I'd change, which is coincidentally ascending order of importance.

1. Disjointness relies on the Cauchy condition in a way I thought was at least as complex and deserved as much attention as the locatedness condition.
2. In the proof of locatedness, you don't need $5\epsilon$, you can substitute $4\epsilon$ without any other changes. (Trivial, but power-of-2 multiplication is slightly easier to put together using addition.)
3. You can substitute $\theta$ wherever $\theta/2$ is used in the rest of the proof, and $\theta/2$ for $\theta/4$.
4. Most importantly, you don't need the locatedness of y at all, in the part beginning "Now either $y < x_\epsilon + \theta/2$ or $x_\epsilon - \theta/2 < y$..." The inequality on the previous line is already all you need; no casework is required.

[mikeshulman]

Nice! Want to submit a PR?

[lowasser]

Was already working on it. Sent!