proposition: Lemma rng_power_mult_law {R : CRing} (x : R) (n m : nat) : (rng_power x n) * (rng_power x m) = rng_power x (n + m).
proof: Proof. induction n as [|n IHn]. 1: apply rng_mult_one_l. refine ((rng_mult_assoc _ _ _)^ @ _). exact (ap (x *.) IHn). Defined.
imports: WildCat Spaces.Nat.Core Classes.interfaces.abstract_algebra Algebra.AbGroups Classes.theory.rings Modalities.ReflectiveSubuniverse