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