feat(algebra/ordered_monoid): sub_neg_monoid (with_top R)

[pechersky]

Before, we had negation on the with_top type only in the case of a linear_ordered_add_comm_monoid_with_top.
But it is possible to provide a no-inverses sub_neg_monoid (with_top R) directly from an
add_group R. We insert it earlier, keeping the same definition of negation.
Some basic API is added as well.

---

[pechersky]

In this PR, I am attempting to define a general sub_add_monoid structure on with_top R when given sub_add_monoid R. I originally thought that one just lifts the subtraction into the modified top, getting the "definitional" lemmas of:

lemma coe_sub [has_sub α] (x y : α) : ((x - y : α) : with_top α) = x - y := rfl
@[simp] lemma top_sub [has_sub α] (x : with_top α) : (⊤ : with_top α) - x = ⊤ := rfl
@[simp] lemma sub_top [has_sub α] (x : with_top α) : x - ⊤ = ⊤ :=
rec_top_coe rfl (λ _, rfl) x

but upon some more thought and encounteringennreal.has_sub,sub_top looks problematic. How I'd like to use this structure is in tropical algebra, and while no text specifies this exactly (as far as I've seen), I think they rely on ⊤ - x ≤ y - ⊤ to be false. That is, something akin to the ennreal.sub definition when subtraction of the top element gives the lowest possible element.

Is subtraction not definable unless working over a has_Inf R? Or should I not even define subtraction on with_top R at all, and define my own div_inv_monoid (tropical (with_top R)) when I have a (conditionally)_complete_linear_order R?

[semorrison]

I simply don't understand this PR, and need more explanation/justification. As far as I understand, with_top A shouldn't have any instances that define negation or subtraction at all, because they don't generally make sense.

If anything, the change we should be making is to remove any existing instances like this, not adding more.

[pechersky]

Thank you for the comments Scott. My hope is to define div_inv_monoid (tropical (with_top R)) when I have a (conditionally)_complete_linear_order R. I will make this and the dependent PR as WIP and revive these when I get to my deeper tropical algebra PRs.

[eric-wieser]

I found myself wanting the analogous instance on has_sub (with_bot A) in a refactor I allude to on Zulip of #12245

[eric-wieser]

Note that we now already have a lemma with this name, but the definition of sub is not the same! It's defined such that a - ⊤ = 0 instead of x - ⊤ = ⊤ as you have here

[pechersky]

I'm happy to trash this PR, I don't know the right way to implement this general instance.