proposition: Lemma Frobenius_aut0 : 0^f = 0.
proof: Proof. by rewrite fE -(prednK (prime_gt0 charf_prime)) exprS mul0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)