[Merged by Bors] - feat: a few lemmas on WithTop ℕ∞

[sgouezel]

To be used when WithTop ℕ∞ becomes the set of smoothness exponents, in #17152

---

[github-actions]

PR summary 8408c6e6a4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ add_one_eq_coe_top_iff
+ add_one_nat_le_withTop_of_lt
+ coe_top_add_one
+ nat_ne_coe_top
+ one_le_iff_ne_zero_withTop

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style