proposition: Lemma nat_pow_exp_mult (x : A) (n m : B) : x ^ (n * m) = (x ^ n) ^ m.
proof: Proof. pattern m. apply naturals.induction; clear m. solve_proper. rewrite right_absorb. now rewrite ?nat_pow_0. intros m E. rewrite nat_pow_S, <-E. rewrite distribute_l, right_identity. now rewrite nat_pow_exp_plus. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations