ideal_product_intersection_sum_subset' (I J : Ideal R) : (I ∩ J) ⋅ (I + J) ⊆ I ⋅ J. Proof. etransitivity. 2: rapply ideal_sum_self. etransitivity. 2: rapply ideal_sum_subset_pres_r. 2: rapply ideal_product_comm. apply ideal_product_intersection_sum_subset. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.