Mult (QuotientAbGroup R I). Proof. srapply Quotient_rec2. - exact (fun x y => class_of _ (x * y)). - intros x x' y p. apply qglue. by apply iscong. - intros x y y' q. apply qglue. by apply iscong. Defined.
Require Import WildCat.Core WildCat.Equiv. Require Import Algebra.Congruence. Require Import Algebra.AbGroups. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Rings.Ring. Require Import Algebra.Rings.Ideal. Import Ideal.Notation.