Unbundled arithmetic typeclasses for Interval friendliness

Interval is not a monoid, so we special type classes if we want to use facts like add_zero. Keeping them unbundled makes things a lot simpler.

class NegZeroClass' (α : Type) [Zero α] [Neg α] : Prop

Unbundled version of NegZeroClass

• neg_zero' : -0 = 0

class AddZeroClass' (α : Type) [Zero α] [Add α] : Prop

Typeclass to express a - 0 = a, 0 - a = -a, without requiring exact monoid structure.

• zero_add' (a : α) : 0 + a = a
• add_zero' (a : α) : a + 0 = a

class SubZeroClass (α : Type) [Zero α] [Neg α] [Sub α] : Prop

Typeclass to express a - 0 = a, 0 - a = -a, without requiring exact monoid structure.

• zero_sub' (a : α) : 0 - a = -a
• sub_zero' (a : α) : a - 0 = a

instance instNegZeroClass' {α : Type} [NegZeroClass α] : NegZeroClass' α

instance instAddZeroClass' {α : Type} [AddZeroClass α] : AddZeroClass' α

instance instSubZeroClass {α : Type} [SubNegZeroMonoid α] : SubZeroClass α