proposition: Lemma expNrz x n : (- x) ^ n = (-1) ^ n * x ^ n :> R.
proof: Proof. case: n=> [] n; rewrite ?NegzE; first exact: exprNn. by rewrite -!exprz_inv !invrN invr1; apply: exprNn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)