proposition: Lemma ideal_sum_smallest (I J K : Ideal R) : I ⊆ K -> J ⊆ K -> (I + J) ⊆ K.
proof: Proof. intros p q. refine (ideal_sum_ind I J (fun x _ => K x) p q _ _). 1: apply ideal_in_zero. intros y z s t. rapply ideal_in_plus_negate. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups