proposition: Lemma exprNn_char x n : (char R).-nat n -> (- x) ^+ n = - (x ^+ n).
proof: Proof. pose p := pdiv n; have [|n_gt1 charRn] := leqP n 1; first by case: (n) => [|[]]. have charRp: p \in char R by rewrite (pnatPpi charRn) // pi_pdiv. have /p_natP[e ->]: p.-nat n by rewrite -(eq_pnat _ (charf_eq charRp)). elim: e => // e IHe; rewrite expnSr !exprM {}IHe. by rewrite -Frobenius_autE Frobenius_autN. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)