Deprecate ltn leq trans

I think it's fine (as stated in the comment) to add ltn_leq_trans, but having a warning message when using it may help users to realize that n < m is just a notation for n.+1 <= m, which can be useful to better use ssrnat.

If this is deemed a bad idea, feel free to just close this merge request.

More generally, there are probably a bunch of things in util that could/should be offered as pull request upstream to MathComp.