Build_CRing' (R : AbGroup) `(!One R, !Mult R) (comm : Commutative (.*.)) (assoc : Associative (.*.)) (dist_l : LeftDistribute (.*.) (+)) (unit_l : LeftIdentity (.*.) 1) : CRing. Proof. snrapply Build_CRing. - rapply (Build_Ring R); only 1,2,4: exact _. + intros x y z. lhs nrapply comm. lhs rapply dist_l. f_ap. + intros x. lhs rapply comm. apply unit_l. - exact _. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.