Commit 2024-09-05 15:25 19f71879

feat(Algebra/Order): rewrite positive cones to use substructure pattern (#15975)

• Rewrite (positive) cones in groups and rings to extend Submonoid and Subsemiring, respectively. This makes them easier to work with in applications.
• Add multiplicative versions of cones in groups.
• Add nonneg constructor for cones from ordered groups/rings.
• Weaken definition of cones in rings slightly (previous definition was nonstandard due to nonstandard definition of linearly ordered ring) -- to compensate, a new fact (ordered domain is strictly ordered domain) has been added.