(I J K : Ideal R) : K ⊆ I -> K ⊆ J -> K ⊆ I ∩ J. Proof. intros p q x r; specialize (p x r); specialize (q x r); by split. 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.