proposition: Lemma Frobenius_autD_comm x y (cxy : comm x y) : (x + y)^f = x^f + y^f.
proof: Proof. have defp := prednK (prime_gt0 charf_prime). rewrite !fE exprDn_comm // big_ord_recr subnn -defp big_ord_recl /= defp. rewrite subn0 mulr1 mul1r bin0 binn big1 ?addr0 // => i _. by rewrite -mulr_natl bin_lt_charf_0 ?mul0r //= -{2}defp ltnS (valP i). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)