mathlib3

98d07d31 - refactor(algebra/order): replace typeclasses with constructors (#9725)

refactor(algebra/order): replace typeclasses with constructors (#9725) This RFC suggests removing some unused classes for the ordered algebra hierarchy, replacing them with constructors We have `nonneg_add_comm_group extends add_comm_group`, and an instance from this to `ordered_add_comm_group`. The intention is to be able to construct an `ordered_add_comm_group` by specifying its positive cone, rather than directly its order. There are then `nonneg_ring` and `linear_nonneg_ring`, similarly. (None of these are actually used later in mathlib at this point.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>