Build_Ring' { ring_abgroup :> AbGroup; ring_mult :: Mult ring_abgroup; ring_one :: One ring_abgroup; ring_isring :: IsRing ring_abgroup; ring_mult_assoc_opp : forall z y x, (x * y) * z = x * (y * z); }.
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.