Extend nonneg_comm_group to support ordered rings specified by their nonnegative elements

Extend nonneg_comm_group to support linearly ordered rings specified by their nonnegative elements