Add lemmas `not_near_inftyP` and `not_near_ninftyP` in `normedtype.v`#1291

Merged

affeldt-aist merged 3 commits intomath-comp:masterfrom Yosuke-Ito-345:add_lemmas_not_near_infty

Aug 20, 2024

+58-21

Commits on Aug 11, 2024

Add-Lemma_not_near_ninftyP

amethyst
authored and
amethyst
committed
trying to exploit symmetry (tentative)
affeldt-aist
committed
don't need to distinguish P and f?
affeldt-aist
committed