Library mathcomp.solvable.burnside_app

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import choice fintype tuple finfun bigop finset fingroup.
From mathcomp Require Import action perm primitive_action.

Application of the Burside formula to count the number of distinct colorings of the vertices of a square and a cube.

Set Implicit Arguments.

Import GroupScope.

Lemma burnside_formula : (gT : finGroupType) s (G : {group gT}),
   uniq s s =i G
    (sT : finType) (to : {action gT &-> sT}),
   (#|orbit to G @: setT| × size s)%N = \sum_(p <- s) #|'Fix_to[p]|.


Section colouring.

Variable n : nat.
Definition colors := 'I_n.
Canonical colors_eqType := Eval hnf in [eqType of colors].
Canonical colors_choiceType := Eval hnf in [choiceType of colors].
Canonical colors_countType := Eval hnf in [countType of colors].
Canonical colors_finType := Eval hnf in [finType of colors].

Section square_colouring.

Definition square := 'I_4.
Canonical square_eqType := Eval hnf in [eqType of square].
Canonical square_choiceType := Eval hnf in [choiceType of square].
Canonical square_countType := Eval hnf in [countType of square].
Canonical square_finType := Eval hnf in [finType of square].
Canonical square_subType := Eval hnf in [subType of square].
Canonical square_subCountType :=
  Eval hnf in [subCountType of square].
Canonical square_subFinType := Eval hnf in [subFinType of square].

Definition mksquare i : square := Sub (i %% _) (ltn_mod i 4).
Definition c0 := mksquare 0.
Definition c1 := mksquare 1.
Definition c2 := mksquare 2.
Definition c3 := mksquare 3.

rotations
Definition R1 (sc : square) : square := tnth [tuple c1; c2; c3; c0] sc.

Definition R2 (sc : square) : square := tnth [tuple c2; c3; c0; c1] sc.

Definition R3 (sc : square) : square := tnth [tuple c3; c0; c1; c2] sc.

Ltac get_inv elt l :=
  match l with
  | (_, (elt, ?x))x
  | (elt, ?x)x
  | (?x, _)get_inv elt x
  end.

Definition rot_inv := ((R1, R3), (R2, R2), (R3, R1)).

Ltac inj_tac :=
  move: (erefl rot_inv); unfold rot_inv;
  match goal with |- ?X = _ injective ?Y
    move_; let x := get_inv Y X in
    apply: (can_inj (g:=x)); move⇒ [val H1]
  end.

Lemma R1_inj : injective R1.

Lemma R2_inj : injective R2.

Lemma R3_inj : injective R3.

Definition r1 := (perm R1_inj).
Definition r2 := (perm R2_inj).
Definition r3 := (perm R3_inj).
Definition id1 := (1 : {perm square}).

Definition is_rot (r : {perm _}) := (r × r1 == r1 × r).
Definition rot := [set r | is_rot r].

Lemma group_set_rot : group_set rot.

Canonical rot_group := Group group_set_rot.

Definition rotations := [set id1; r1; r2; r3].

Lemma rot_eq_c0 : r s : {perm square},
  is_rot r is_rot s r c0 = s c0 r = s.

Lemma rot_r1 : r, is_rot r r = r1 ^+ (r c0).

Lemma rotations_is_rot : r, r \in rotations is_rot r.

Lemma rot_is_rot : rot = rotations.

symmetries
Definition Sh (sc : square) : square := tnth [tuple c1; c0; c3; c2] sc.

Lemma Sh_inj : injective Sh.

Definition sh := (perm Sh_inj).

Lemma sh_inv : sh^-1 = sh.

Definition Sv (sc : square) : square := tnth [tuple c3; c2; c1; c0] sc.

Lemma Sv_inj : injective Sv.

Definition sv := (perm Sv_inj).

Lemma sv_inv : sv^-1 = sv.

Definition Sd1 (sc : square) : square := tnth [tuple c0; c3; c2; c1] sc.

Lemma Sd1_inj : injective Sd1.

Definition sd1 := (perm Sd1_inj).

Lemma sd1_inv : sd1^-1 = sd1.

Definition Sd2 (sc : square) : square := tnth [tuple c2; c1; c0; c3] sc.

Lemma Sd2_inj : injective Sd2.

Definition sd2 := (perm Sd2_inj).

Lemma sd2_inv : sd2^-1 = sd2.

Lemma ord_enum4 : enum 'I_4 = [:: c0; c1; c2; c3].

Lemma diff_id_sh : 1 != sh.

Definition isometries2 := [set 1; sh].

Lemma card_iso2 : #|isometries2| = 2.

Lemma group_set_iso2 : group_set isometries2.
Canonical iso2_group := Group group_set_iso2.

Definition isometries :=
  [set p | [|| p == 1, p == r1, p == r2, p == r3,
            p == sh, p == sv, p == sd1 | p == sd2 ]].

Definition opp (sc : square) := tnth [tuple c2; c3; c0; c1] sc.

Definition is_iso (p : {perm square}) := ci, p (opp ci) = opp (p ci).

Lemma isometries_iso : p, p \in isometries is_iso p.

Ltac non_inj p a1 a2 heq1 heq2 :=
let h1:= fresh "h1" in
(absurd (p a1 = p a2); first (by red ⇒ - h1; move: (perm_inj h1));
by rewrite heq1 heq2; apply/eqP).

Ltac is_isoPtac p f e0 e1 e2 e3 :=
  suff ->: p = f by [rewrite inE eqxx ?orbT];
  let e := fresh "e" in apply/permP;
  do 5?[case] ⇒ // ?; [move: e0 | move: e1 | move: e2 | move: e3] ⇒ e;
  apply: etrans (congr1 p _) (etrans e _); apply/eqP; rewrite // permE.

Lemma is_isoP : p, reflect (is_iso p) (p \in isometries).

Lemma group_set_iso : group_set isometries.

Canonical iso_group := Group group_set_iso.

Lemma card_rot : #|rot| = 4.

Lemma group_set_rotations : group_set rotations.

Canonical rotations_group := Group group_set_rotations.

Notation col_squares := {ffun square colors}.

Definition act_f (sc : col_squares) (p : {perm square}) : col_squares :=
  [ffun z sc (p^-1 z)].

Lemma act_f_1 : k, act_f k 1 = k.

Lemma act_f_morph : k x y, act_f k (x × y) = act_f (act_f k x) y.

Definition to := TotalAction act_f_1 act_f_morph.

Definition square_coloring_number2 := #|orbit to isometries2 @: setT|.
Definition square_coloring_number4 := #|orbit to rotations @: setT|.
Definition square_coloring_number8 := #|orbit to isometries @: setT|.

Lemma Fid : 'Fix_to(1) = setT.

Lemma card_Fid : #|'Fix_to(1)| = (n ^ 4)%N.

Definition coin0 (sc : col_squares) : colors := sc c0.
Definition coin1 (sc : col_squares) : colors := sc c1.
Definition coin2 (sc : col_squares) : colors := sc c2.
Definition coin3 (sc : col_squares) : colors := sc c3.

Lemma eqperm_map : p1 p2 : col_squares,
  (p1 == p2) = all (fun sp1 s == p2 s) [:: c0; c1; c2; c3].

Lemma F_Sh :
  'Fix_to[sh] = [set x | (coin0 x == coin1 x) && (coin2 x == coin3 x)].

Lemma F_Sv :
  'Fix_to[sv] = [set x | (coin0 x == coin3 x) && (coin2 x == coin1 x)].

Ltac inv_tac :=
  apply: esym (etrans _ (mul1g _)); apply: canRL (mulgK _) _;
  let a := fresh "a" in apply/permPa;
  apply/eqP; rewrite permM !permE; case: a; do 4?case.

Lemma r1_inv : r1^-1 = r3.

Lemma r2_inv : r2^-1 = r2.

Lemma r3_inv : r3^-1 = r1.

Lemma F_r2 :
  'Fix_to[r2] = [set x | (coin0 x == coin2 x) && (coin1 x == coin3 x)].

Lemma F_r1 : 'Fix_to[r1] =
  [set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&&(coin2 x == coin3 x)].

Lemma F_r3 : 'Fix_to[r3] =
  [set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&&(coin2 x == coin3 x)].

Lemma card_n2 : x y z t : square, uniq [:: x; y; z; t]
  #|[set p : col_squares | (p x == p y) && (p z == p t)]| = (n ^ 2)%N.

Lemma card_n :
 #|[set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&& (coin2 x == coin3 x)]|
   = n.

Lemma burnside_app2 : (square_coloring_number2 × 2 = n ^ 4 + n ^ 2)%N.

Lemma burnside_app_rot :
  (square_coloring_number4 × 4 = n ^ 4 + n ^ 2 + 2 × n)%N.

Lemma F_Sd1 : 'Fix_to[sd1] = [set x | coin1 x == coin3 x].

Lemma card_n3 : x y : square, x != y
  #|[set k : col_squares | k x == k y]| = (n ^ 3)%N.

Lemma F_Sd2 : 'Fix_to[sd2] = [set x | coin0 x == coin2 x].

Lemma burnside_app_iso :
  (square_coloring_number8 × 8 = n ^ 4 + 2 × n ^ 3 + 3 × n ^ 2 + 2 × n)%N.

End square_colouring.

Section cube_colouring.

Definition cube := 'I_6.
Canonical cube_eqType := Eval hnf in [eqType of cube].
Canonical cube_choiceType := Eval hnf in [choiceType of cube].
Canonical cube_countType := Eval hnf in [countType of cube].
Canonical cube_finType := Eval hnf in [finType of cube].
Canonical cube_subType := Eval hnf in [subType of cube].
Canonical cube_subCountType := Eval hnf in [subCountType of cube].
Canonical cube_subFinType := Eval hnf in [subFinType of cube].

Definition mkFcube i : cube := Sub (i %% 6) (ltn_mod i 6).
Definition F0 := mkFcube 0.
Definition F1 := mkFcube 1.
Definition F2 := mkFcube 2.
Definition F3 := mkFcube 3.
Definition F4 := mkFcube 4.
Definition F5 := mkFcube 5.

axial symetries
Definition S05 := [:: F0; F4; F3; F2; F1; F5].
Definition S05f (sc : cube) : cube := tnth [tuple of S05] sc.

Definition S14 := [:: F5; F1; F3; F2; F4; F0].
Definition S14f (sc : cube) : cube := tnth [tuple of S14] sc.

Definition S23 := [:: F5; F4; F2; F3; F1; F0].
Definition S23f (sc : cube) : cube := tnth [tuple of S23] sc.

rotations 90
Definition R05 := [:: F0; F2; F4; F1; F3; F5].
Definition R05f (sc : cube) : cube := tnth [tuple of R05] sc.
Definition R50 := [:: F0; F3; F1; F4; F2; F5].
Definition R50f (sc : cube) : cube := tnth [tuple of R50] sc.
Definition R14 := [:: F3; F1; F0; F5; F4; F2].
Definition R14f (sc : cube) : cube := tnth [tuple of R14] sc.
Definition R41 := [:: F2; F1; F5; F0; F4; F3].
Definition R41f (sc : cube) : cube := tnth [tuple of R41] sc.
Definition R23 := [:: F1; F5; F2; F3; F0; F4].
Definition R23f (sc : cube) : cube := tnth [tuple of R23] sc.
Definition R32 := [:: F4; F0; F2; F3; F5; F1].
Definition R32f (sc : cube) : cube := tnth [tuple of R32] sc.
rotations 120
Definition R024 := [:: F2; F5; F4; F1; F0; F3].
Definition R024f (sc : cube) : cube := tnth [tuple of R024] sc.
Definition R042 := [:: F4; F3; F0; F5; F2; F1].
Definition R042f (sc : cube) : cube := tnth [tuple of R042] sc.
Definition R012 := [:: F1; F2; F0; F5; F3; F4].
Definition R012f (sc : cube) : cube := tnth [tuple of R012] sc.
Definition R021 := [:: F2; F0; F1; F4; F5; F3].
Definition R021f (sc : cube) : cube := tnth [tuple of R021] sc.
Definition R031 := [:: F3; F0; F4; F1; F5; F2].
Definition R031f (sc : cube) : cube := tnth [tuple of R031] sc.
Definition R013 := [:: F1; F3; F5; F0; F2; F4].
Definition R013f (sc : cube) : cube := tnth [tuple of R013] sc.
Definition R043 := [:: F4; F2; F5; F0; F3; F1].
Definition R043f (sc : cube) : cube := tnth [tuple of R043] sc.
Definition R034 := [:: F3; F5; F1; F4; F0; F2].
Definition R034f (sc : cube) : cube := tnth [tuple of R034] sc.
last symmetries
Definition S1 := [:: F5; F2; F1; F4; F3; F0].
Definition S1f (sc : cube) : cube := tnth [tuple of S1] sc.
Definition S2 := [:: F5; F3; F4; F1; F2; F0].
Definition S2f (sc : cube) : cube := tnth [tuple of S2] sc.
Definition S3 := [:: F1; F0; F3; F2; F5; F4].
Definition S3f (sc : cube) : cube := tnth [tuple of S3] sc.
Definition S4 := [:: F4; F5; F3; F2; F0; F1].
Definition S4f (sc : cube) : cube := tnth [tuple of S4] sc.
Definition S5 := [:: F2; F4; F0; F5; F1; F3].
Definition S5f (sc : cube) : cube := tnth [tuple of S5] sc.
Definition S6 := [::F3; F4; F5; F0; F1; F2].
Definition S6f (sc : cube) : cube := tnth [tuple of S6] sc.

Lemma S1_inv : involutive S1f.

Lemma S2_inv : involutive S2f.

Lemma S3_inv : involutive S3f.

Lemma S4_inv : involutive S4f.

Lemma S5_inv : involutive S5f.

Lemma S6_inv : involutive S6f.

Lemma S05_inj : injective S05f.

Lemma S14_inj : injective S14f.

Lemma S23_inv : involutive S23f.

Lemma R05_inj : injective R05f.

Lemma R14_inj : injective R14f.

Lemma R23_inj : injective R23f.

Lemma R50_inj : injective R50f.

Lemma R41_inj : injective R41f.

Lemma R32_inj : injective R32f.

Lemma R024_inj : injective R024f.

Lemma R042_inj : injective R042f.

Lemma R012_inj : injective R012f.

Lemma R021_inj : injective R021f.

Lemma R031_inj : injective R031f.

Lemma R013_inj : injective R013f.

Lemma R043_inj : injective R043f.

Lemma R034_inj : injective R034f.

Definition id3 := 1 : {perm cube}.

Definition s05 := (perm S05_inj).

Definition s14 : {perm cube}.

Definition s23 := (perm (inv_inj S23_inv)).
Definition r05 := (perm R05_inj).
Definition r14 := (perm R14_inj).
Definition r23 := (perm R23_inj).
Definition r50 := (perm R50_inj).
Definition r41 := (perm R41_inj).
Definition r32 := (perm R32_inj).
Definition r024 := (perm R024_inj).
Definition r042 := (perm R042_inj).
Definition r012 := (perm R012_inj).
Definition r021 := (perm R021_inj).
Definition r031 := (perm R031_inj).
Definition r013 := (perm R013_inj).
Definition r043 := (perm R043_inj).
Definition r034 := (perm R034_inj).

Definition s1 := (perm (inv_inj S1_inv)).
Definition s2 := (perm (inv_inj S2_inv)).
Definition s3 := (perm (inv_inj S3_inv)).
Definition s4 := (perm (inv_inj S4_inv)).
Definition s5 := (perm (inv_inj S5_inv)).
Definition s6 := (perm (inv_inj S6_inv)).

Definition dir_iso3 := [set p |
[|| id3 == p, s05 == p, s14 == p, s23 == p, r05 == p, r14 == p, r23 == p,
 r50 == p, r41 == p, r32 == p, r024 == p, r042 == p, r012 == p, r021 == p,
 r031 == p, r013 == p, r043 == p, r034 == p,
 s1 == p, s2 == p, s3 == p, s4 == p, s5 == p | s6 == p]].

Definition dir_iso3l := [:: id3; s05; s14; s23; r05; r14; r23; r50; r41;
  r32; r024; r042; r012; r021; r031; r013; r043; r034;
  s1; s2; s3; s4; s5; s6].

Definition S0 := [:: F5; F4; F3; F2; F1; F0].
Definition S0f (sc : cube) : cube := tnth [tuple of S0] sc.

Lemma S0_inv : involutive S0f.

Definition s0 := (perm (inv_inj S0_inv)).

Definition is_iso3 (p : {perm cube}) := fi, p (s0 fi) = s0 (p fi).

Lemma dir_iso_iso3 : p, p \in dir_iso3 is_iso3 p.

Lemma iso3_ndir : p, p \in dir_iso3 is_iso3 (s0 × p).

Definition sop (p : {perm cube}) : seq cube := fgraph (val p).

Lemma sop_inj : injective sop.

Definition prod_tuple (t1 t2 : seq cube) :=
  map (fun n : 'I_6nth F0 t2 n) t1.

Lemma sop_spec x (n0 : 'I_6): nth F0 (sop x) n0 = x n0.

Lemma prod_t_correct : (x y : {perm cube}) (i : cube),
  (x × y) i = nth F0 (prod_tuple (sop x) (sop y)) i.

Lemma sop_morph : {morph sop : x y / x × y >-> prod_tuple x y}.

Definition ecubes : seq cube := [:: F0; F1; F2; F3; F4; F5].

Lemma ecubes_def : ecubes = enum (@predT cube).

Definition seq_iso_L := [::
   [:: F0; F1; F2; F3; F4; F5];
   S05; S14; S23; R05; R14; R23; R50; R41; R32;
   R024; R042; R012; R021; R031; R013; R043; R034;
   S1; S2; S3; S4; S5; S6].

Lemma seqs1 : f injf, sop (@perm _ f injf) = map f ecubes.

Lemma Lcorrect : seq_iso_L == map sop [:: id3; s05; s14; s23; r05; r14; r23;
  r50; r41; r32; r024; r042; r012; r021; r031; r013; r043; r034;
  s1; s2; s3; s4; s5; s6].

Lemma iso0_1 : dir_iso3 =i dir_iso3l.

Lemma L_iso : p, (p \in dir_iso3) = (sop p \in seq_iso_L).

Lemma stable : x y,
  x \in dir_iso3 y \in dir_iso3 x × y \in dir_iso3.

Lemma iso_eq_F0_F1 : r s : {perm cube}, r \in dir_iso3
  s \in dir_iso3 r F0 = s F0 r F1 = s F1 r = s.

Lemma ndir_s0p : p, p \in dir_iso3 s0 × p \notin dir_iso3.

Definition indir_iso3l := map (mulg s0) dir_iso3l.

Definition iso3l := dir_iso3l ++ indir_iso3l.

Definition seq_iso3_L := map sop iso3l.

Lemma eqperm : p1 p2 : {perm cube},
  (p1 == p2) = all (fun sp1 s == p2 s) ecubes.

Lemma iso_eq_F0_F1_F2 : r s : {perm cube}, is_iso3 r
   is_iso3 s r F0 = s F0 r F1 = s F1 r F2 = s F2 r = s.

Ltac iso_tac :=
  let a := fresh "a" in apply/permPa;
  apply/eqP; rewrite !permM !permE; case: a; do 6?case.

Ltac inv_tac :=
  apply: esym (etrans _ (mul1g _)); apply: canRL (mulgK _) _; iso_tac.

Lemma dir_s0p : p, (s0 × p) \in dir_iso3 p \notin dir_iso3.

Definition is_iso3b p := (p × s0 == s0 × p).
Definition iso3 := [set p | is_iso3b p].

Lemma is_iso3P : p, reflect (is_iso3 p) (p \in iso3).

Lemma group_set_iso3 : group_set iso3.

Canonical iso_group3 := Group group_set_iso3.

Lemma group_set_diso3 : group_set dir_iso3.
Canonical diso_group3 := Group group_set_diso3.

Lemma gen_diso3 : dir_iso3 = <<[set r05; r14]>>.

Notation col_cubes := {ffun cube colors}.

Definition act_g (sc : col_cubes) (p : {perm cube}) : col_cubes :=
  [ffun z sc (p^-1 z)].

Lemma act_g_1 : k, act_g k 1 = k.

Lemma act_g_morph : k x y, act_g k (x × y) = act_g (act_g k x) y.

Definition to_g := TotalAction act_g_1 act_g_morph.

Definition cube_coloring_number24 := #|orbit to_g diso_group3 @: setT|.

Lemma Fid3 : 'Fix_to_g[1] = setT.

Lemma card_Fid3 : #|'Fix_to_g[1]| = (n ^ 6)%N.

Definition col0 (sc : col_cubes) : colors := sc F0.
Definition col1 (sc : col_cubes) : colors := sc F1.
Definition col2 (sc : col_cubes) : colors := sc F2.
Definition col3 (sc : col_cubes) : colors := sc F3.
Definition col4 (sc : col_cubes) : colors := sc F4.
Definition col5 (sc : col_cubes) : colors := sc F5.

Lemma eqperm_map2 : p1 p2 : col_cubes,
  (p1 == p2) = all (fun sp1 s == p2 s) [:: F0; F1; F2; F3; F4; F5].

Notation infE := (sameP afix1P eqP).

Lemma F_s05 :
  'Fix_to_g[s05] = [set x | (col1 x == col4 x) && (col2 x == col3 x)].

Lemma F_s14 :
   'Fix_to_g[s14]= [set x | (col0 x == col5 x) && (col2 x == col3 x)].

Lemma r05_inv : r05^-1 = r50.

Lemma r50_inv : r50^-1 = r05.

Lemma r14_inv : r14^-1 = r41.

Lemma r41_inv : r41^-1 = r14.

Lemma s23_inv : s23^-1 = s23.

Lemma F_s23 :
  'Fix_to_g[s23] = [set x | (col0 x == col5 x) && (col1 x == col4 x)].

Lemma F_r05 : 'Fix_to_g[r05]=
  [set x | (col1 x == col2 x) && (col2 x == col3 x)
                                && (col3 x == col4 x)].

Lemma F_r50 : 'Fix_to_g[r50]=
  [set x | (col1 x == col2 x) && (col2 x == col3 x)
                                && (col3 x == col4 x)].

Lemma F_r23 : 'Fix_to_g[r23] =
  [set x | (col0 x == col1 x) && (col1 x == col4 x)
                                && (col4 x == col5 x)].

Lemma F_r32 : 'Fix_to_g[r32] =
  [set x | (col0 x == col1 x) && (col1 x == col4 x)
                                && (col4 x == col5 x)].

Lemma F_r14 : 'Fix_to_g[r14] =
  [set x | (col0 x == col2 x) && (col2 x == col3 x) && (col3 x == col5 x)].

Lemma F_r41 : 'Fix_to_g[r41] =
  [set x | (col0 x == col2 x) && (col2 x == col3 x) && (col3 x == col5 x)].

Lemma F_r024 : 'Fix_to_g[r024] =
  [set x | (col0 x == col4 x) && (col4 x == col2 x) && (col1 x == col3 x)
       && (col3 x == col5 x) ].

Lemma F_r042 : 'Fix_to_g[r042] =
  [set x | (col0 x == col4 x) && (col4 x == col2 x) && (col1 x == col3 x)
       && (col3 x == col5 x)].

Lemma F_r012 : 'Fix_to_g[r012] =
  [set x | (col0 x == col2 x) && (col2 x == col1 x) && (col3 x == col4 x)
       && (col4 x == col5 x)].

Lemma F_r021 : 'Fix_to_g[r021] =
  [set x | (col0 x == col2 x) && (col2 x == col1 x) && (col3 x == col4 x)
       && (col4 x == col5 x)].

Lemma F_r031 : 'Fix_to_g[r031] =
  [set x | (col0 x == col3 x) && (col3 x == col1 x) && (col2 x == col4 x)
       && (col4 x == col5 x)].

Lemma F_r013 : 'Fix_to_g[r013] =
  [set x | (col0 x == col3 x) && (col3 x == col1 x) && (col2 x == col4 x)
       && (col4 x == col5 x)].

Lemma F_r043 : 'Fix_to_g[r043] =
  [set x | (col0 x == col4 x) && (col4 x == col3 x) && (col1 x == col2 x)
       && (col2 x == col5 x)].

Lemma F_r034 : 'Fix_to_g[r034] =
  [set x | (col0 x == col4 x) && (col4 x == col3 x) && (col1 x == col2 x)
       && (col2 x == col5 x)].

Lemma F_s1 : 'Fix_to_g[s1] =
  [set x | (col0 x == col5 x) && (col1 x == col2 x) && (col3 x == col4 x)].

Lemma F_s2 : 'Fix_to_g[s2] =
  [set x | (col0 x == col5 x) && (col1 x == col3 x) && (col2 x == col4 x)].

Lemma F_s3 : 'Fix_to_g[s3] =
  [set x | (col0 x == col1 x) && (col2 x == col3 x) && (col4 x == col5 x)].

Lemma F_s4 : 'Fix_to_g[s4] =
  [set x | (col0 x == col4 x) && (col1 x == col5 x) && (col2 x == col3 x)].

Lemma F_s5 : 'Fix_to_g[s5] =
  [set x | (col0 x == col2 x) && (col1 x == col4 x) && (col3 x == col5 x)].

Lemma F_s6 : 'Fix_to_g[s6] =
  [set x | (col0 x == col3 x) && (col1 x == col4 x) && (col2 x == col5 x)].

Lemma uniq4_uniq6 : x y z t : cube,
  uniq [:: x; y; z; t] u, v, uniq [:: x; y; z; t; u; v].

Lemma card_n4 : x y z t : cube, uniq [:: x; y; z; t]
   #|[set p : col_cubes | (p x == p y) && (p z == p t)]| = (n ^ 4)%N.

Lemma card_n3_3 : x y z t: cube, uniq [:: x; y; z; t]
  #|[set p : col_cubes | (p x == p y) && (p y == p z)&& (p z == p t)]|
      = (n ^ 3)%N.

Lemma card_n2_3 : x y z t u v: cube, uniq [:: x; y; z; t; u; v]
  #|[set p : col_cubes | (p x == p y) && (p y == p z)&& (p t == p u )
                            && (p u== p v)]| = (n ^ 2)%N.

Lemma card_n3s : x y z t u v: cube, uniq [:: x; y; z; t; u; v]
  #|[set p : col_cubes | (p x == p y) && (p z == p t)&& (p u == p v )]|
    = (n ^ 3)%N.

Lemma burnside_app_iso3 :
  (cube_coloring_number24 × 24 =
                   n ^ 6 + 6 × n ^ 3 + 3 × n ^ 4 + 8 × (n ^ 2) + 6 × n ^ 3)%N.

End cube_colouring.

End colouring.

Corollary burnside_app_iso_3_3col: cube_coloring_number24 3 = 57.

Corollary burnside_app_iso_2_4col: square_coloring_number8 4 = 55.