proposition: Lemma burnside_app_iso : (square_coloring_number8 * 8 = n ^ 4 + 2 * n ^ 3 + 3 * n ^ 2 + 2 * n)%N.
proof: Proof. pose iso_list := [:: id1; r1; r2; r3; sh; sv; sd1; sd2]. rewrite (burnside_formula iso_list) => [||p]; last first. - by rewrite /= !inE. - apply: map_uniq (fun p : {perm square} => (p c0, p c1)) _ _. by rewrite /= !permE. rewrite !big_cons big_nil {1}card_Fid F_r1 F_r2 F_r3 F_Sh F_Sv F_Sd1 F_Sd2. by rewrite card_n !card_n3 // !card_n2 //=; 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)