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!)
Version 2.1.8p2
