{R : Ring} (x : R) (n m : nat) : (rng_power x n) * (rng_power x m) = rng_power x (n + m). Proof. induction n as [|n IHn]. 1: apply rng_mult_one_l. refine ((rng_mult_assoc _ _ _)^ @ _). exact (ap (x *.) IHn). Defined.
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.