{R : CRing} (x y z : R) : x * y * z = x * z * y. Proof. lhs_V nrapply rng_mult_assoc. rhs_V nrapply rng_mult_assoc. apply ap, rng_mult_comm. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.