proposition: Lemma burnside_app_iso3 : (cube_coloring_number24 * 24 = n ^ 6 + 6 * n ^ 3 + 3 * n ^ 4 + 8 * (n ^ 2) + 6 * n ^ 3)%N.
proof: Proof. pose iso_list := [:: id3; s05; s14; s23; r05; r14; r23; r50; r41; r32; r024; r042; r012; r021; r031; r013; r043; r034; s1; s2; s3; s4; s5; s6]. rewrite (burnside_formula iso_list); last first. - by move=> p; rewrite !inE /= !(eq_sym _ p). - apply: map_uniq (fun p : {perm cube} => (p F0, p F1)) _ _. have bsr : (fun p : {perm cube} => (p F0, p F1)) =1 (fun p => (nth F0 p F0, nth F0 p F1)) \o sop. by move=> x; rewrite /= -2!sop_spec. by rewrite (eq_map bsr) map_comp -(eqP Lcorrect); vm_compute. rewrite !big_cons big_nil {1}card_Fid3 /= F_s05 F_s14 F_s23 F_r05 F_r14 F_r23 F_r50 F_r41 F_r32 F_r024 F_r042 F_r012 F_r021 F_r031 F_r013 F_r043 F_r034 F_s1 F_s2 F_s3 F_s4 F_s5 F_s6. by rewrite !card_n4 // !card_n3_3 // !card_n2_3 // !card_n3s //; ring. 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)