proposition: Lemma int_pow_negate (x : A) (n : B) : x ^ (-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.negate_0, int_pow_0, dec_recip_1. rewrite 2!int_pow_base_0; trivial. now rewrite dec_recip_0. now apply rings.flip_negate_ne_0. revert n. apply biinduction. solve_proper. now rewrite rings.negate_0, int_pow_0, dec_recip_1. intros n. setoid_replace (-n) with (1 - (1 + n)) by ring. rewrite 2!int_pow_S, dec_recip_distr; trivial. split; intros E. rewrite <-E. now field. rewrite E, associativity, dec_recip_inverse; trivial. ring. 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