Hard to fix Stdlib arithmetic deprecations in 8.18 breaking many projects in 8.19

Description of the problem

Pierre Castéran and I have recently tried to fix many Stdlib arithmetic deprecation warnings in Coq 8.18 to avoid projects breaking in 8.19 due to coq/coq#18164. However, we have determined that some, specifically those related to Nat.add_sub and Nat.sub_add require significant work and are thus likely to break many projects forever. The following example is due to @Casteran:

Require Import Arith.
Require Import ArithRing.

Goal forall a b c d,  a <= d ->
                      a * b + (a * (c - b) +
                                 (d * (c - b) - a * (c - b)))
                      + d * b =
                        (d + a) * b + d * (c - b).
intros a b c d H.
rewrite (le_plus_minus_r).
(*
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default]
*)
  - ring.
  - now apply Nat.mul_le_mono_r.
Restart.
    (* lets apply the Hint *)
intros a b c d H.
 rewrite Nat.add_comm. (* needs more precision ! *)
 Fail rewrite Nat.sub_add.
Abort.

We believe Stdlib maintainers and release managers should seriously consider ensuring deprecated/removed lemmas requiring a combination of Nat.sub_add/Nat.add_sub and Nat.add_comm like le_plus_minus_r are added verbatim under Nat, e.g., Nat.le_plus_minus_r, cc: @SkySkimmer @olaure01

If coq/coq#18355 was implemented, the severity of this problem would be significantly reduced.

Coq Version

Deprecations show up in 8.18.0 and projects break in 8.19+rc1.

Start by reproducing the shown Coq script and reviewing the deprecation messages for le_plus_minus_r, Nat.add_sub, and Nat.sub_add. The issue proposes adding compatible Nat lemmas; done means the arithmetic migration no longer requires brittle combinations of Nat.sub_add and Nat.add_comm and affected projects avoid breaking in 8.19.