(I J K : Ideal R) : I ⊆ J -> (K + I) ⊆ (K + J). Proof. intros p. apply ideal_sum_smallest. 1: apply ideal_sum_subset_l. transitivity J. 1: exact p. apply ideal_sum_subset_r. 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.