@IsCongruence R ring_mult (in_cosetL I). Proof. snrapply Build_IsCongruence. intros x x' y y' p q. change (I ( - (x * y) + (x' * y'))). rewrite <- (rng_plus_zero_l (x' * y')). rewrite <- (rng_plus_negate_r (x' * y)). rewrite 2 rng_plus_assoc. rewrite <- rng_mult_negate_l. rewrite <- rng_dist_r. rewrite <- rng_plus_assoc. rewrite <- rng_mult_negate_r. rewrite <- rng_dist_l. rapply subgroup_in_op. - by rapply isrightideal. - by rapply isleftideal. 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.