Commit 2026-08-25 15:52 211ee653
View on Github →feat(EReal): add_eq_top_iff_eq_top_* (#41288)
Adds add_eq_top_iff_eq_top_{left,right} and replaces the proofs of the ne versions with .ne. add_ne_top_iff_of_ne_bot_of_ne_top was duplicated, so I deprecated it.