There is a general proof of (b) above.

For *any* commutative closed monoidal preorder we have

\[ x \multimap y \otimes y \multimap z \le x \multimap z \]

We don't really care if we are in \\(\mathbf{Bool}\\) or \\(\mathbf{Cost}\\) or whatever.

First observe

\[ a \multimap b \le a \multimap b \text{ for all } a \text{ and } b\]

This follows from reflexivity of \\(\le\\). By the adjointness of \\(\otimes \dashv\, \multimap\\) we know

\[ a \multimap b \otimes a \le b \text{ for all } a \text{ and } b\]

In particular, we have

\[
\begin{align}
x \multimap y \otimes x & \le y \tag{A}\\\\
y \multimap z \otimes y & \le z \tag{B}
\end{align}
\]

If we take \\((A)\\), we can *tensor* both sides by applying \\(y \multimap z\, \otimes \\) to get

\[
y \multimap z \otimes x \multimap y \otimes x \le y \multimap z \otimes y
\]

This follows since \\(\otimes\\) is monotone. Along with \\((B)\\) and transitivity of \\(\le\\) we have

\[
y \multimap z \otimes x \multimap y \otimes x \le z
\]

applying \\(\otimes \dashv\, \multimap\\) once again to this gives

\[
y \multimap z \otimes x \multimap y \le x \multimap z \tag{★}
\]

Finally, since we are assuming \\(\otimes\\) is commutative, we know

\[
y \multimap z \otimes x \multimap y = x \multimap y \otimes y \multimap z
\]

taking this along with \\((★)\\) finally yields:

\[
x \multimap y \otimes y \multimap z \le x \multimap z
\]