\ralf{Copy the rest of the explanation from the paper, when that one is more polished.}
\ralf{Copy the rest of the explanation from the paper, when that one is more polished.}
\paragraph{The division operation$\mdiv$.}
\paragraph{The division operator$\mdiv$.}
One way to describe $\mdiv$ is to say that it extracts the witness from the extension order: If $\melt\leq\meltB$, then $\melt\mdiv\meltB$ computes the difference between the two elements (\ruleref{cmra-div-op}).
One way to describe $\mdiv$ is to say that it extracts the witness from the extension order: If $\melt\leq\meltB$, then $\melt\mdiv\meltB$ computes the difference between the two elements (\ruleref{cmra-div-op}).
Otherwise, $\mdiv$ can have arbitrary behavior.
Otherwise, $\mdiv$ can have arbitrary behavior.
This means that, in classical logic, the division operator can be defined for any PCM using the axiom of choice, and it will trivially satisfy \ruleref{cmra-div-op}.
This means that, in classical logic, the division operator can be defined for any PCM using the axiom of choice, and it will trivially satisfy \ruleref{cmra-div-op}.
