archimedean): add `sub` variations of `add` lemmas (#18103)

Commit

3 years ago

chore(algebra/order/archimedean): add `sub` variations of `add` lemmas (#18103) These spellings give the intuition of "reduce"ing to a range rather than "lifting" to a range.

Author

eric-wieser

Parents

e017e666

mathlib3 6f413f3f - chore(algebra/order/archimedean): add `sub` variations of `add` lemmas (#18103)

mathlib3
6f413f3f - chore(algebra/order/archimedean): add `sub` variations of `add` lemmas (#18103)