proposition: Lemma card_finField_unit (F : finFieldType) : #|[set: {unit F}]| = #|F|.-1.
proof: Proof. by rewrite -(cardC1 0) cardsT card_sub; apply: eq_card => x; rewrite GRing.unitfE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype finset fingroup morphism perm action) mathcomp(ssralg countalg)