How to transparently manage different naming schemes, or different ordering of arguments, etc. in libraries?

This was already discussed here and there, but, motivated by coq/coq#6282, let me open an explicit issue to collect potential discussions.

There are many lemmas here and there in the community, especially about standard structures such as lists, or natural, integer, rational, real arithmetic. The standard library itself mixes different naming schemes, e.g. the

• nat-specific style S_pred
• vs a more generic style lt_succ_pred,

and different conventions in formulating a statement, e.g. the

• iff style as in succ_lt_mono: forall n m, n < m <-> succ n < succ m
• vs an impl style as in lt_S_n : forall n m, S n < S m -> n < m and lt_n_S: forall n m, n < m -> S n < S m

or in the order of expressions in equality, the

• -> -rewriting style of lt_succ_pred : forall n m, m < n -> succ (pred n) = n
• vs the "destructable" style of S_pred : forall n m, m < n -> n = succ (pred n))

etc.

Morally, all this is equivalent. Morally, we should be able to find easily a needed lemma whether it is in the standard library, in math-comp, in TLC, in coq-std++, in a local library, in one of the miscellaneous MoreList files that many users add to their development (e.g. here), etc. (Not talking about the long-term goal of building a "universal" library of (possibly "big") proofs.)

So, how to make progress in the direction of transparently supporting superficially-heterogenous styles, whether is it in searching or using lemmas, etc?

Start by reviewing the naming and statement examples in the standard library, then compare the linked math-comp, TLC, coq-std++, and MoreList resources. Identify a concrete approach for finding or applying equivalent lemmas across conventions; done requires a decided scope and an agreed implementation path.