feat(algebra/ordered_monoid): add_eq_bot_iff (#8474)
bot addition is saturating on the bottom. On the way, typeclass arguments
were relaxed to just `[add_semigroup α]`, and helper simp lemmas
added for `bot`.
The iff lemma added (`add_eq_bot`) is not exactly according to the naming convention, but matches the top lemma and related ones in the naming style, so the style is kept consistent.
There is an API proof available, but the defeq proof (using the top equivalent) was used based on suggestions.
