proposition: Lemma int_pow_negate_alt (x : A) (n : B) : x ^ n = /(x ^ (-n)).
proof: Proof. rewrite <-int_pow_negate. now rewrite rings.negate_involutive. 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