fact: Record CRing := { cring_type : Type; cring_plus : Plus cring_type; cring_mult : Mult cring_type; cring_zero : Zero cring_type; cring_one : One cring_type; cring_negate : Negate cring_type; cring_isring : IsRing cring_type; }.
imports: WildCat Spaces.Nat.Core Classes.interfaces.abstract_algebra Algebra.AbGroups Classes.theory.rings Modalities.ReflectiveSubuniverse