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
\]