proposition: Lemma ideal_quotient_product_left (I J : Ideal R) : (I :: J) ⋅ J ⊆ I.
proof: Proof. by apply ideal_quotient_subset_prod. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups