Ring -> Ring. Proof. intros [R mult one [is_abgroup [[monoid_ishset mult_assoc] li ri] ld rd] mult_assoc_opp]. snrapply Build_Ring'. 4: split. 5: split. 5: split. - exact R. - exact (fun x y => mult y x). - exact one. - exact is_abgroup. - exact monoid_ishset. - exact mult_assoc_opp. - exact ri. - exact li. - exact (fun x y z => rd y z x). - exact (fun x y z => ld z x y). - exact mult_assoc. 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.