mathlib3

7507876b - feat(data/real/ereal): `coe : ℝ → ereal` is strictly monotone (#16607)

feat(data/real/ereal): `coe : ℝ → ereal` is strictly monotone (#16607) and golf existing lemmas with it. Also delete `ereal.bot_lt_top` and friends in terms of the more general `bot_lt_top`.