(R : AbGroup) `(Mult R, One R, !Associative (.*.), !LeftDistribute (.*.) (+), !RightDistribute (.*.) (+), !LeftIdentity (.*.) 1, !RightIdentity (.*.) 1) : Ring. Proof. rapply (' R). 2: exact (fun z y x => (associativity x y z)^). split; only 1,3,4: exact _. repeat split; exact _. Defined.
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.