]
qed.
-(* \ 5h2 class="section"\ 6Mixing proofs and computations\ 5/h2\ 6
+(*
+\ 5h2 class="section"\ 6Mixing proofs and computations\ 5/h2\ 6
There is still another possibility, however, namely to mix the program and its
specification into a single entity. The idea is to refine the output type of the
div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers but a