proposition: Lemma nat_pow_base_mult (x y : A) (n : B) : (x * y) ^ n = x ^ n * y ^ n.
proof: Proof. pattern n. apply naturals.induction; clear n. solve_proper. rewrite ?nat_pow_0. ring. intros n E. rewrite ?nat_pow_S. rewrite E. ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations