chore(data/real/{e,}nnreal): a few lemmas (#5530)
* Rename `nnreal.le_of_forall_lt_one_mul_lt` to
`nnreal.le_of_forall_lt_one_mul_le`, and similarly for `ennreal`.
* Move the proof of the latter lemma to `topology/instances/ennreal`,
prove it using continuity of multiplication.
* Add `ennreal.le_of_forall_nnreal_lt`, `nnreal.lt_div_iff`, and
`nnreal.mul_lt_of_lt_div`.
