proposition: Lemma ideal_product_subset_pres_r (I J K : Ideal R) : I ⊆ J -> K ⋅ I ⊆ K ⋅ J.
proof: Proof. intros p r q. strip_truncations. induction q as [r i | | r s ]. + destruct i. apply tr, sgt_in, ipn_in. 2: apply p. 1,2: assumption. + 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