(I J : Ideal R) : (I :: J) ⋅ J ⊆ I. Proof. by apply ideal_quotient_subset_prod. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.