proposition: Lemma powRN x r : x `^ (- r) = (x `^ r)^-1.
proof: Proof. have [r0|r0] := eqVneq r 0%R; first by rewrite r0 oppr0 powRr0 invr1. have [->|xN0] := eqVneq x 0; first by rewrite !powR0 ?oppr_eq0// invr0. rewrite -div1r; apply: (canRL (mulfK _)); first by rewrite powR_eq0 (negPf xN0). by rewrite -powRD ?addNr ?powRr0// xN0 eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex