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