proposition: Lemma ideal_product_intersection_sum_subset (I J : Ideal R) : (I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + J ⋅ I).
proof: Proof. etransitivity. 1: rapply ideal_dist_l. etransitivity. 1: rapply ideal_sum_subset_pres_r. 1: rapply ideal_product_subset_pres_l. 1: apply ideal_intersection_subset_l. etransitivity. 1: rapply ideal_sum_subset_pres_l. 1: rapply ideal_product_subset_pres_l. 1: apply ideal_intersection_subset_r. rapply ideal_sum_comm. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups