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.

Thanks, Pierre! The change is fine with me.

I don't have a good sense for what parts of util might be interesting for upstream. If you point out which lemmas seem worthwhile, I'd be happy to help prepare MRs against mathcomp.

assigned to @bbb

resolved all threads

merged