(I J K : Ideal R) : (I :: J) :: K ↔ (I :: (J ⋅ K)). Proof. apply ideal_subset_antisymm. - intros x [p q]; strip_truncations; split; apply tr; intros r; rapply Trunc_rec; intros jk. + induction jk as [y [z z' j k] | | ? ? ? ? ? ? ]. * rewrite (rng_mult_comm z z'). rewrite rng_mult_assoc. destruct (p z' k) as [p' ?]. revert p'; apply Trunc_rec; intros p'. exact (p' z j). * change (I (x * 0)). rewrite rng_mult_zero_r. apply ideal_in_zero. * change (I (x * (g - h))). rewrite rng_dist_l. rewrite rng_mult_negate_r. by apply ideal_in_plus_negate. + induction jk as [y [z z' j k] | | ? ? ? ? ? ? ]. * change (I (z * z' * x)). rewrite <- rng_mult_assoc. rewrite (rng_mult_comm z). destruct (q z' k) as [q' ?]. revert q'; apply Trunc_rec; intros q'. exact (q' z j). * change (I (0 * x)). rewrite rng_mult_zero_l. apply ideal_in_zero. * change (I ((g - h) * x)). rewrite rng_dist_r. rewrite rng_mult_negate_l. by apply ideal_in_plus_negate. - intros x [p q]; strip_truncations; split; apply tr; intros r k; split; apply tr; intros z j. + rewrite <- rng_mult_assoc. rewrite (rng_mult_comm r z). by apply p, tr, sgt_in, ipn_in. + cbn in z. change (I (z * (x * r))). rewrite (rng_mult_comm x). rewrite rng_mult_assoc. by apply q, tr, sgt_in, ipn_in. + cbn in r. change (I (r * x * z)). rewrite <- rng_mult_assoc. rewrite (rng_mult_comm r). rewrite <- rng_mult_assoc. by apply p, tr, sgt_in, ipn_in. + cbn in r, z. change (I (z * (r * x))). rewrite rng_mult_assoc. rewrite rng_mult_comm. by apply p, tr, sgt_in, ipn_in. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.