I think we can simplify that slightly @Matthew

We have your (A) and (B), ie \\(x\otimes (x\multimap y) \leq y\\) and \\(y \otimes (y\multimap z) \leq z\\).

Therefore \\(x\otimes (x\multimap y) \otimes (y\multimap z) \leq y \otimes (y\multimap z) \leq z\\).

So by adjunction \\((x\multimap y) \otimes (y\multimap z) \leq (x\multimap z)\\).

(EDIT: Oh I see this is the same proof, but you spelled it out in a bit more detail!)

We have your (A) and (B), ie \\(x\otimes (x\multimap y) \leq y\\) and \\(y \otimes (y\multimap z) \leq z\\).

Therefore \\(x\otimes (x\multimap y) \otimes (y\multimap z) \leq y \otimes (y\multimap z) \leq z\\).

So by adjunction \\((x\multimap y) \otimes (y\multimap z) \leq (x\multimap z)\\).

(EDIT: Oh I see this is the same proof, but you spelled it out in a bit more detail!)