proposition: Lemma burnside_app_rot : (square_coloring_number4 * 4 = n ^ 4 + n ^ 2 + 2 * n)%N.
proof: Proof. rewrite (burnside_formula [:: id1; r1; r2; r3]) => [||p]; last first. - by rewrite !inE !orbA. - by apply: map_uniq (fun p : {perm square} => p c0) _ _; rewrite /= !permE. rewrite !big_cons big_nil /= addn0 {1}card_Fid F_r1 F_r2 F_r3. by rewrite card_n 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)