{ cring_ring :> Ring; cring_commutative :: Commutative (A:=cring_ring) (.*.); }.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.