proposition: Lemma Frobenius_autMn x n : (x *+ n)^f = x^f *+ n.
proof: Proof. elim: n => [|n IHn]; first exact: Frobenius_aut0. by rewrite !mulrS Frobenius_autD_comm ?IHn //; apply: commrMn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)