(I J K : Ideal R) : I ⊆ K -> J ⊆ K -> (I + J) ⊆ K. 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.
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.