{R : Ring} (r : R) (n : cring_Z) : rng_int_mult R r n = (rng_int_mult R 1 n) * r. Proof. cbn. rhs nrapply (grp_pow_natural (grp_homo_rng_right_mult r)); cbn. by rewrite rng_mult_one_l. Defined.
Require Import Classes.interfaces.canonical_names. Require Import Algebra.AbGroups. Require Import Algebra.Rings.CRing. Require Import Spaces.Int Spaces.Pos. Require Import WildCat.Core.