IsRing (QuotientAbGroup R I). Proof. split. 1: exact _. 1: repeat split. 1: exact _. { srapply Quotient_ind3_hprop; intros x y z. unfold sg_op, mult_is_sg_op, mult_quotient_group; simpl. apply ap. apply associativity. } 1,2: snrapply Quotient_ind_hprop; [exact _ | intro x]. 1-2: unfold sg_op, mult_is_sg_op, mult_quotient_group; simpl. 1-2: apply ap. 1: apply left_identity. 1: apply right_identity. { srapply Quotient_ind3_hprop; intros x y z. unfold sg_op, mult_is_sg_op, mult_quotient_group, plus, mult, plus_quotient_group; simpl. apply ap. apply simple_distribute_l. } { srapply Quotient_ind3_hprop; intros x y z. unfold sg_op, mult_is_sg_op, mult_quotient_group, plus, mult, plus_quotient_group; simpl. apply ap. apply simple_distribute_r. } 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.