Commit 2022-09-29 01:02 0ec98ed0
View on Github →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.