mathlib3

b9762673 - chore(data/real/ennreal): deduplicate `ennreal.nat_ne_top` (#15853)

chore(data/real/ennreal): deduplicate `ennreal.nat_ne_top` (#15853) The lemmas `ennreal.nat_ne_top` and `ennreal.coe_nat_ne_top` are near duplicates, with the former being a `simp` lemma taking an explicit argument, and the latter being a non-`simp` lemma taking an implicit argument. The former is used slightly more frequently (in explicit form) in mathlib. We remove `ennreal.coe_nat_ne_top` in favor of `ennreal.nat_ne_top`.