        </p>
                </td>
<td>
                  <p>
                    pre: there exists a value <code class="computeroutput"><span class="identifier">n</span></code>
                    of <code class="computeroutput"><span class="identifier">Distance</span></code> such
                    that <code class="computeroutput"><span class="identifier">a</span> <span class="special">+</span>
                    <span class="identifier">n</span> <span class="special">==</span>
                    <spa