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

\]

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

\]