Add the lemma not_near_ninftyP in normedtype.v

[Yosuke-Ito-345]

Motivation for this change

@affeldt-aist
Add an infinite version of the lemma not_near_at_rightP in normedtype.v.
Tell me if I should write a change log in CHANGELOG_UNRELEASED.md.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md
• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[hoheinzollern]

Nice work!
I'm unsure about the naming, since the P suffix suggests that you move between bool and prop, but the lemma actually changes the statement.
Once the naming is settled, you can add that to CHANGELOG_UNRELEASED.md on a new line.

[Yosuke-Ito-345]

@hoheinzollern
Thank you for the review!
I know that P is often used for reflection lemmas, but I adopted the suffix for the following reasons.

1. The contributing guide of mathcomp says that P can be used for a characteristic property.
2. The similar lemma not_near_at_rightP uses the same suffix, but this is not a reflection lemma.

If P should not be used in my case, that probably means I misunderstand something. Do I really need to drop P?

[hoheinzollern]

Ok, that's a pretty valid argument. Would it make sense to add a similar lemma for not_near_inftyP?

[Yosuke-Ito-345]

Thank you very much.
As you pointed out, I will add the lemma not_near_inftyP after this pull request is approved.
I also consider generalizing the lemmas not_near_at_rightP and not_near_at_leftP (cf. issue #1723).

I added my lemma in CHANGELOG_UNRELEASED.md, but GitHub says that there are conflicts. Should I make another changelog file?

[affeldt-aist]

It is maybe better if you provide all the similar-looking lemmas in the same PR: their mutual comparison could help figure out better names and potential factorizations.

As for the changelog conflict, you can do a rebase.

[Yosuke-Ito-345]

All right. Thanks for the advice.
I will formalize not_near_inftyP later, and reflect it to this pull request.

[Yosuke-Ito-345]

Sorry, I could not solve my conflict problem by rebase.
(Maybe I did something completely wrong, but I am not sure...)

I created a new pull request, so could you please review the new one?
I will delete this pull request (#1280) when everything has done.

[affeldt-aist]

note that you can add closes issue #1280 to the PR message of the new PR to close this issue automatically

[Yosuke-Ito-345]

I didn't know that!
Thanks for teaching me such a convenient command.

[affeldt-aist]

the same contents have made their way into master through the merged PR #1291