(I J : Ideal R) : (I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + J ⋅ I). 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.
Require Import Basics Types. Require Import Spaces.Finite.Fin. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Rings.Ring. Require Import Algebra.Groups.Subgroup. Require Import Algebra.AbGroups. Require Import WildCat.Core. Module Import Notation.