`leq_addr` vs `ltn_addr` (and `addl` variants)

I noticed that there are some strange statement/naming inconsistencies in ssrnat.v

leq_addr: forall m n : nat, n <= n + m
ltn_addr: forall [m n : nat] (p : nat), m < n -> m < n + p

besides the fact that these two lemmas differ in more than replacing _ <= _ with _ < _, the second lemma is also needlessly restricting the shape of the left-hand side to _.+1. I stumbled across this while looking for

Lemma leq_addr? m n p : m <= n -> m <= n + p

which appears to be missing. How should this lemma be named? :thinking:

(the same applies to leq_addl and ltn_addl.)

I know! Disturbing, right?

So you knew and choose not to do anything about it?

So you knew and choose not to do anything about it?

Well, the asymmetry can be justified since ltn_addr has no short form, and for the rare occurrences where the long form of leq_addr was helpful, I simply did (leq_trans _ (łeq_addr _ _)), so maybe a proper name would be leq_trans_addr?

Well, why have ltn_addr in the first place, this is just an instance of the long form of leq_addr with m := m.+1

Well, why have ltn_addr in the first place, this is just an instance of the long form of leq_addr with m := m.+1

Sure thing!

So what's the course of action, if any? Remove/deprecate ltn_addr in favor of a long form for leq_addr? How should this long form be named?

Let's name the long form leq_trans_addr and deprecate leq_addr, and then remove the latter, and switch from leq_trans_addr to leq_addr, if replacing leq_addr by leq_trans_addr does not cause too much overhead.

@CohenCyril @chdoc some news on this issue?