\input{header}
\begin{document}
\begin{theorem}
If
\begin{eqnarray}
\label{A0}
\mathsf{p \cdot q} & =& \mathsf{q \cdot r}
\end{eqnarray}
then\[\mathsf{p\star \cdot q = q \cdot r\star}\]
\end{theorem}By antisym, it suffices to show that
\begin{eqnarray}
\label{T75}
\mathsf{p\star \cdot q} & \leq& \mathsf{q \cdot r\star}\\
\label{T76}
\mathsf{q \cdot r\star} & \leq& \mathsf{p\star \cdot q}
\end{eqnarray}
Consider (\ref{T75}).  By *R, it suffices to show that
\begin{eqnarray}
\label{T77}
\mathsf{p \cdot q \cdot r\star + q} & \leq& \mathsf{q \cdot r\star}
\end{eqnarray}
Consider (\ref{T77}).  By unwindL, we know that
\begin{eqnarray*}
\mathsf{q \cdot r\star} & =& \mathsf{q \cdot (1 + r \cdot r\star)}
\end{eqnarray*}By distrL, we know that
\begin{eqnarray*}
\mathsf{q \cdot (1 + r \cdot r\star)} & =& \mathsf{q \cdot 1 + q \cdot r \cdot r\star}
\end{eqnarray*}By id.R, we know that
\begin{eqnarray*}
\mathsf{q \cdot 1 + q \cdot r \cdot r\star} & =& \mathsf{q + q \cdot r \cdot r\star}
\end{eqnarray*}By commut+, we know that
\begin{eqnarray*}
\mathsf{q + q \cdot r \cdot r\star} & =& \mathsf{q \cdot r \cdot r\star + q}
\end{eqnarray*}By mono+R, it suffices to show that
\begin{eqnarray}
\label{T82}
\mathsf{p \cdot q \cdot r\star} & \leq& \mathsf{q \cdot r \cdot r\star}
\end{eqnarray}
Consider (\ref{T82}).  By mono.R, it suffices to show that
\begin{eqnarray}
\label{T83}
\mathsf{p \cdot q} & \leq& \mathsf{q \cdot r}
\end{eqnarray}
Consider (\ref{T83}).  By =<, it suffices to show that
\begin{eqnarray}
\label{T84}
\mathsf{p \cdot q} & =& \mathsf{q \cdot r}
\end{eqnarray}
Consider (\ref{T84}).  By (\ref{A0}), we have what we need.
Consider (\ref{T76}).  By *L, it suffices to show that
\begin{eqnarray}
\label{T85}
\mathsf{p\star \cdot q \cdot r + q} & \leq& \mathsf{p\star \cdot q}
\end{eqnarray}
Consider (\ref{T85}).  By unwindR, we know that
\begin{eqnarray*}
\mathsf{p\star \cdot q} & =& \mathsf{(1 + p\star \cdot p) \cdot q}
\end{eqnarray*}By distrR, we know that
\begin{eqnarray*}
\mathsf{(1 + p\star \cdot p) \cdot q} & =& \mathsf{1 \cdot q + p\star \cdot p \cdot q}
\end{eqnarray*}By commut+, we know that
\begin{eqnarray*}
\mathsf{1 \cdot q + p\star \cdot p \cdot q} & =& \mathsf{p\star \cdot p \cdot q + 1 \cdot q}
\end{eqnarray*}By id.L, we know that
\begin{eqnarray*}
\mathsf{p\star \cdot p \cdot q + 1 \cdot q} & =& \mathsf{p\star \cdot p \cdot q + q}
\end{eqnarray*}By mono+R, it suffices to show that
\begin{eqnarray}
\label{T90}
\mathsf{p\star \cdot q \cdot r} & \leq& \mathsf{p\star \cdot p \cdot q}
\end{eqnarray}
Consider (\ref{T90}).  By mono.L, it suffices to show that
\begin{eqnarray}
\label{T91}
\mathsf{q \cdot r} & \leq& \mathsf{p \cdot q}
\end{eqnarray}
Consider (\ref{T91}).  By =<, it suffices to show that
\begin{eqnarray}
\label{T92}
\mathsf{q \cdot r} & =& \mathsf{p \cdot q}
\end{eqnarray}
Consider (\ref{T92}).  By sym, it suffices to show that
\begin{eqnarray}
\label{T93}
\mathsf{p \cdot q} & =& \mathsf{q \cdot r}
\end{eqnarray}
Consider (\ref{T93}).  By (\ref{A0}), we have what we need.
$\Box$
\end{document}