(I J K : Ideal R) : I ⋅ J ⊆ K <-> I ⊆ (K :: J). Proof. split. - intros p r i; split; apply tr; intros s j; cbn in s, r. + by apply p, tr, sgt_in, ipn_in. + change (K (s * r)). rewrite (rng_mult_comm s r). by apply p, tr, sgt_in; rapply ipn_in. - intros p x. apply Trunc_rec. intros q. induction q as [r x | | ]. { destruct x. specialize (p x s); destruct p as [p q]. revert p; apply Trunc_rec; intros p. by apply p. } 1: apply ideal_in_zero. by apply ideal_in_plus_negate. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.