proposition: Lemma Frobenius_autN x : (- x)^f = - x^f.
proof: Proof. apply/eqP; rewrite -subr_eq0 opprK addrC. by rewrite -(Frobenius_autD_comm _ (commrN _)) // subrr Frobenius_aut0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)