proposition: Lemma rng_power_mult {R : CRing} (x y : R) (n : nat) : rng_power (x * y) n = rng_power x n * rng_power y n.
proof: Proof. induction n. 1: symmetry; apply rng_mult_one_l. simpl. rewrite rng_mult_assoc. rewrite <- (rng_mult_assoc x _ y). rewrite (rng_mult_comm (rng_power x n) y). rewrite rng_mult_assoc. rewrite <- (rng_mult_assoc _ (rng_power x n)). f_ap. Defined.
imports: WildCat Spaces.Nat.Core Classes.interfaces.abstract_algebra Algebra.AbGroups Classes.theory.rings Modalities.ReflectiveSubuniverse