{R : Ring} {I J : Ideal R} (p : (I ↔ J)%ideal) : R / I ≅ R / J. Proof. snrapply Build_RingIsomorphism'. { srapply equiv_quotient_functor'. 1: exact equiv_idmap. intros x y; cbn. apply p. } repeat split. 1,2: srapply Quotient_ind2_hprop; intros x y; rapply qglue. 1: change (J ( - (x + y) + (x + y))). 2: change (J (- ( x * y) + (x * y))). 1,2: rewrite rng_plus_negate_l. 1,2: apply ideal_in_zero. 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.