proposition: Lemma ideal_quotient_product (I J K : Ideal R) : (I :: J) :: K ↔ (I :: (J ⋅ K)).
proof: Proof. apply ideal_subset_antisymm. { hnf. intros x p y q. cbv in p. strip_truncations. induction q as [y i | | ]. - destruct i as [ y z s t ]. rewrite (rng_mult_comm y). rewrite rng_mult_assoc. by apply p. - rewrite rng_mult_zero_r. apply ideal_in_zero. - rewrite rng_dist_l. rewrite rng_mult_negate_r. by apply ideal_in_plus_negate. } intros x p y k z j; hnf in p. rewrite <- rng_mult_assoc. rewrite (rng_mult_comm y). by apply p, tr, sgt_in, ipn_in. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups