{R : CRing} (x y z : R) : x * (y * z) = y * (x * z). Proof. refine (rng_mult_assoc _ _ _ @ _ @ (rng_mult_assoc _ _ _)^). apply rng_mult_move_left_assoc. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.