proposition: Lemma ideal_product_subset_r (I J : Ideal R) : I ⋅ J ⊆ J.
proof: Proof. intros r p. strip_truncations. induction p as [r i | | r s p1 IHp1 p2 IHp2 ]. + destruct i as [s t]. by apply isideal. + rapply ideal_in_zero. + by rapply ideal_in_plus_negate. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups