proposition: Lemma burnside_app2 : (square_coloring_number2 * 2 = n ^ 4 + n ^ 2)%N.
proof: Proof. rewrite (burnside_formula [:: id1; sh]) => [||p]; last first. - by rewrite !inE. - by rewrite /= inE diff_id_sh. by rewrite 2!big_cons big_nil addn0 {1}card_Fid F_Sh card_n2. 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)