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$