(I J K : Ideal R) : I ⊆ J -> K ⋅ I ⊆ K ⋅ J. Proof. intros p r q. strip_truncations. induction q as [r i | | r s ]. + destruct i. apply tr, sgt_in, ipn_in. 2: apply p. 1,2: assumption. + apply ideal_in_zero. + by apply 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.