{R : CRing} (x y z : R) : x * y * z = y * x * z. Proof. f_ap; apply rng_mult_comm. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.