proposition: Lemma nat_pow_recip `{DecField A} `{Naturals B} `{!NatPowSpec A B pw} : (∀ x y : A, Decision (x = y)) -> forall (a : A) (n : B), (/a) ^ n = /(a ^ n).
proof: Proof. intros D a. apply naturals.induction. + intros n1 n2 E; now rewrite E. + rewrite !nat_pow_0; symmetry; apply dec_recip_1. + intros n IH. now rewrite !nat_pow_S, dec_recip_distr, IH. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.QArith MathClasses.implementations.stdlib_rationals CoRN.model.structures.Qinf CoRN.model.structures.Qpossec CoRN.model.structures.QposInf CoRN.model.structures.QnonNeg MathClasses.interfaces.abstract_algebra MathClasses.implementations.QType_rationals MathClasses.interfaces.additional_operations CoRN.tactics.Qauto Coq.QArith.QOrderedType MathClasses.theory.rings MathClasses.theory.dec_fields MathClasses.orders.rings MathClasses.orders.dec_fields MathClasses.theory.nat_pow MathClasses.interfaces.naturals MathClasses.interfaces.orders CoRN.reals.fast.CRGeometricSum CoRN.ode.metric