proposition: Lemma card_Fid3 : #|'Fix_to_g[1]| = (n ^ 6)%N.
proof: Proof. rewrite -[6]card_ord -[n]card_ord -card_ffun_on Fid3 cardsT. by symmetry; apply: eq_card => ff; apply/ffun_onP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset fingroup) mathcomp(action perm primitive_action)