proposition: Lemma ideal_quotient_subset_prod (I J K : Ideal R) : I ⋅ J ⊆ K <-> I ⊆ (K :: J).
proof: Proof. split. { intros p r i s j. by apply p, tr, sgt_in, ipn_in. } intros p x q. strip_truncations. induction q as [r x | | ]. { destruct x. cbv in p. by apply p. } 1: apply ideal_in_zero. by apply ideal_in_plus_negate. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups