(I J : Ideal R) : I ⊆ J -> Ann J ⊆ Ann I. Proof. intros p x [q q']; hnf in q, q'; strip_truncations; split; apply tr; intros y i. - by apply q, p. - by apply q', p. 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.