proposition: Lemma exprDn_char x y n : (char R).-nat n -> (x + y) ^+ n = x ^+ n + y ^+ 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{charRn} /p_natP[e ->]: p.-nat n by rewrite -(eq_pnat _ (charf_eq charRp)). by elim: e => // e IHe; rewrite !expnSr !exprM IHe -Frobenius_autE rmorphD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)