(I J : Ideal R) : I ⋅ J ⊆ I. Proof. intros r p. strip_truncations. induction p as [r i | | r s p1 IHp1 p2 IHp2 ]. + destruct i as [s t]. by rapply isrightideal. + rapply ideal_in_zero. + by 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.