proposition: Lemma expN1r (i : int) : (-1 : R) ^ i = (-1) ^+ `|i|.
proof: Proof. case: i => n; first by rewrite exprnP absz_nat. by rewrite NegzE abszN absz_nat -invr_expz expfV invrN1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)