\ralf{Copy the rest of the explanation from the paper, when that one is more polished.}
\paragraph{The division operation $\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}).
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}.
However, notice that the division operator also has to be \emph{non-expansive} --- so if the carrier $\monoid$ is equipped with a non-trivial $\nequiv{n}$, there is an additional proof obligation here.
This is crucial, for the following reason:
Considering that the extension order is defined using \emph{equality}, there is a natural notion of a \emph{step-indexed extension} order using the step-indexed equivalence of the underlying COFE:
One of the properties we would expect to hold is the usual correspondence between a step-indexed predicate and its non-step-indexed counterpart:
\[\All\melt, \meltB. \melt\leq\meltB\Lra(\All n. \melt\mincl{n}\meltB)\tagH{cmra-incl-limit}\]
The right-to-left direction here is trick.
For every $n$, we obtain a proof that $\melt\mincl{n}\meltB$.
From this, we could extract a sequence of witnesses $(\meltC_m)_{m}$, and we need to arrive at a single witness $\meltC$ showing that $\melt\leq\meltB$.
Without the division operator, there is no reason to believe that such a witness exists.
However, since we can use the division operator, and since we know that this operator is \emph{non-expansive}, we can pick $\meltC\eqdef\meltB\mdiv\melt$, and then we can prove that this is indeed the desired witness.
\ralf{Do we actually need this property anywhere?}
\node (b12) at (1.7, -1) {$\meltB_1\mtimes\meltB_2$};
\node (a12) at (0, -1) {$\melt_1\mtimes\melt_2$};
\path (a) edge node {$\nequiv{n}$} (b);
\path (a12) edge node {$\nequiv{n}$} (b12);
\path (a) edge node [rotate=90] {$=$} (a12);
\path (b) edge node [rotate=90] {$=$} (b12);
\end{tikzpicture}\end{center}
where the $n$-equivalence at the bottom is meant to apply to the pairs of elements, \ie we demand $\melt_1\nequiv{n}\meltB_1$ and $\melt_2\nequiv{n}\meltB_2$.
In other words, extension carries the decomposition of $\meltB$ into $\meltB_1$ and $\meltB_2$ over the $n$-equivalence of $\melt$ and $\meltB$, and yields a corresponding decomposition of $\melt$ into $\melt_1$ and $\melt_2$.
This operation is needed to prove that $\later$ commutes with existential quantification and separating conjunction:
