proposition: Lemma int_pow_exp_mult (x : A) (n m : B) : x ^ (n * m) = (x ^ n) ^ m.
proof: Proof. destruct (decide (x = 0)) as [Ex|Ex]. rewrite Ex. destruct (decide (n = 0)) as [En|En]. rewrite En, left_absorb, int_pow_0. now rewrite left_absorb. destruct (decide (m = 0)) as [Em|Em]. now rewrite Em, right_absorb, 2!int_pow_0. rewrite 3!int_pow_base_0; try easy. intros E. now destruct (zero_product n m E). revert m. apply biinduction. solve_proper. rewrite right_absorb. now rewrite 2!int_pow_0. intros m. split; intros E. rewrite int_pow_S, <-E. rewrite distribute_l, right_identity. now rewrite int_pow_exp_plus. now apply int_pow_ne_0. rewrite int_pow_S in E. rewrite distribute_l, right_identity, int_pow_exp_plus in E. apply (rings.left_cancellation_ne_0 (.*.) (x ^ n)). now apply int_pow_ne_0. now rewrite E. easy. now apply int_pow_ne_0. 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