proposition: Lemma fin_little_fermat (F : finFieldType) (n c : nat) : n \in [char F] -> c%:R ^+ n = c%:R :> F.
proof: Proof. move=> nC. have Pp : prime n by apply: charf_prime nC. have Cn : [char F].-nat n by rewrite pnatE. elim: c => [|c IH]; first by rewrite -natrX exp0n ?prime_gt0. by rewrite -addn1 natrD exprDn_char // IH -natrX exp1n. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)