mathlib3

0ec98ed0 - refactor(data/real/ereal): `sub_neg_zero_monoid` instance (#16688)

refactor(data/real/ereal): `sub_neg_zero_monoid` instance (#16688) Add a `sub_neg_zero_monoid` instance for `ereal`, so eliminating its `neg_zero`, `sub_zero` and `sub_eq_add_neg` lemmas and allowing results for `neg_zero_class` to be applied to `ereal`.