{R : Ring} (r : R) (n : cring_Z) : rng_int_mult R r n = r * (rng_int_mult R 1 n). Proof. cbn. rhs nrapply (grp_pow_natural (grp_homo_rng_left_mult r)); cbn. by rewrite rng_mult_one_r. 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.