(I J : Ideal R) : I ⋅ J ⊆ J ⋅ I. Proof. intros r p. strip_truncations. induction p as [r p | |]. 2: apply ideal_in_zero. 2: by apply ideal_in_plus_negate. destruct p as [s t p q]. rewrite rng_mult_comm. apply tr. apply sgt_in. by rapply ipn_in. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.