proposition: Lemma int_pow_nat_pow `{Naturals N} `{!NatPowSpec A N pw} {f : N → B} `{!SemiRing_Morphism f} (x : A) (n : N) : x ^ (f n) = x ^ n.
proof: Proof. revert n. apply naturals.induction. solve_proper. now rewrite rings.preserves_0, int_pow_0, nat_pow_0. intros n E. rewrite rings.preserves_plus, rings.preserves_1. rewrite int_pow_S_nonneg, nat_pow_S. now rewrite E. apply semirings.preserves_nonneg. now apply naturals.nat_nonneg. Qed.
imports: Coq.setoid_ring.Ring Coq.setoid_ring.Field MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.theory.nat_pow MathClasses.theory.int_abs MathClasses.theory.dec_fields