proposition: Lemma preserves_int_pow_exp x (n : B1) : x ^ (f n) = x ^ n.
proof: Proof. destruct (decide (x = 0)) as [Ex | Ex]. rewrite Ex. destruct (decide (n = 0)) as [En|En]. now rewrite En, rings.preserves_0, 2!int_pow_0. rewrite 2!int_pow_base_0; try easy. now apply rings.injective_ne_0. revert n. apply biinduction. solve_proper. rewrite rings.preserves_0. now rewrite 2!int_pow_0. intros n. rewrite rings.preserves_plus, rings.preserves_1. rewrite 2!int_pow_S by trivial. split; intros E. now rewrite E. now apply (rings.left_cancellation_ne_0 (.*.) x). 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