(I J : Ideal R) : ideal_unit R ⊆ (I + J) -> I ∩ J ⊆ I ⋅ J. Proof. intros p. etransitivity. { apply ideal_eq_subset. symmetry. apply ideal_product_unit_r. } etransitivity. 1: rapply (ideal_product_subset_pres_r _ _ _ p). rapply ideal_product_intersection_sum_subset'. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.