CRing. Proof. snrapply Build_CRing'. - exact abgroup_Z. - exact 1%int. - exact int_mul. - exact int_mul_comm. - exact int_mul_assoc. - exact int_dist_l. - exact int_mul_1_l. Defined.
Require Import Classes.interfaces.canonical_names. Require Import Algebra.AbGroups. Require Import Algebra.Rings.CRing. Require Import Spaces.Int Spaces.Pos. Require Import WildCat.Core.