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.

src/algebra/ordered_monoid.lean

@@ -494,9 +494,13 @@ by norm_cast
 lemma coe_bit1 [add_semigroup α] [has_one α] {a : α} : ((bit1 a : α) : with_bot α) = bit1 a :=
 by norm_cast
 
-@[simp] lemma bot_add [ordered_add_comm_monoid α] (a : with_bot α) : ⊥ + a = ⊥ := rfl
+@[simp] lemma bot_add [add_semigroup α] (a : with_bot α) : ⊥ + a = ⊥ := rfl
 
-@[simp] lemma add_bot [ordered_add_comm_monoid α] (a : with_bot α) : a + ⊥ = ⊥ := by cases a; refl
+@[simp] lemma add_bot [add_semigroup α] (a : with_bot α) : a + ⊥ = ⊥ := by cases a; refl
+
+@[simp] lemma add_eq_bot [add_semigroup α] {m n : with_bot α} :
+  m + n = ⊥ ↔ m = ⊥ ∨ n = ⊥ :=
+with_top.add_eq_top
 
 end with_bot
 

src/order/bounded_lattice.lean

@@ -449,6 +449,9 @@ instance : inhabited (with_bot α) := ⟨⊥⟩
 lemma none_eq_bot : (none : with_bot α) = (⊥ : with_bot α) := rfl
 lemma some_eq_coe (a : α) : (some a : with_bot α) = (↑a : with_bot α) := rfl
 
+@[simp] theorem bot_ne_coe (a : α) : ⊥ ≠ (a : with_bot α) .
+@[simp] theorem coe_ne_bot (a : α) : (a : with_bot α) ≠ ⊥ .
+
 /-- Recursor for `with_bot` using the preferred forms `⊥` and `↑a`. -/
 @[elab_as_eliminator]
 def rec_bot_coe {C : with_bot α → Sort*} (h₁ : C ⊥) (h₂ : Π (a : α), C a) :