proposition: Lemma int_pow_recip (x : A) (n : B) : (/x) ^ n = /(x ^ n).
proof: Proof. destruct (decide (x = 0)) as [Ex | Ex]. rewrite Ex, dec_recip_0. destruct (decide (n = 0)) as [En | En]. now rewrite En, int_pow_0, dec_recip_1. now rewrite int_pow_base_0, dec_recip_0. revert n. apply biinduction. solve_proper. now rewrite 2!int_pow_0, dec_recip_1. intros n. assert (/x ≠ 0) by now apply dec_recip_ne_0. rewrite 2!int_pow_S, dec_recip_distr; 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