(R : CRing) (I : Ideal R) : CRing := Build_CRing (QuotientRing R I) _.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.