{R : CRing} (x y : R) (n : nat) : rng_power (R:=R) (x * y) n = rng_power (R:=R) x n * rng_power (R:=R) y n. Proof. induction n. 1: symmetry; rapply rng_mult_one_l. simpl. rewrite (rng_mult_assoc (A:=R)). rewrite <- (rng_mult_assoc (A:=R) x _ y). rewrite (rng_mult_comm (rng_power (R:=R) x n) y). rewrite rng_mult_assoc. rewrite <- (rng_mult_assoc _ (rng_power (R:=R) x n)). f_ap. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.