proposition: Lemma preserves_nat_pow x (n : B) : f (x ^ n) = (f x) ^ n.
proof: Proof. revert n. apply naturals.induction. solve_proper. rewrite nat_pow_0, nat_pow_0. now apply rings.preserves_1. intros n E. rewrite nat_pow_S, rings.preserves_mult, E. now rewrite nat_pow_S. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations