proposition: Lemma ideal_quotient_subset (I J : Ideal R) : I ⊆ (I :: J).
proof: Proof. intros x i r j. rewrite rng_mult_comm. by apply isideal. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups