proposition: Lemma nat_pow_exp_plus (x : A) (n m : B) : x ^ (n + m) = x ^ n * x ^ m.
proof: Proof. pattern n. apply naturals.induction; clear n. solve_proper. rewrite nat_pow_0, left_identity. ring. intros n E. rewrite <-associativity. rewrite 2!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