proposition: Lemma card_n3 : forall x y : square, x != y -> #|[set k : col_squares | k x == k y]| = (n ^ 3)%N.
proof: Proof. move=> x y nxy; apply/eqP; case: (posnP n) => [n0|]. by rewrite n0; apply/existsP=> [] [p _]; case: (p c0) => i; rewrite n0. move/eqn_pmul2l <-; rewrite -expnS -card_Fid Fid cardsT. rewrite -{1}[n]card_ord -cardX. pose pk k := [ffun i => k (if i == y then x else i) : colors]. rewrite -(@card_image _ _ (fun k : col_squares => (k y, pk k))). apply/eqP; apply: eq_card => ck /=; rewrite inE /= [_ \in _]inE. apply/eqP/imageP; last first. by case=> k _ -> /=; rewrite !ffunE if_same eqxx. case: ck => c k /= kxy. exists [ffun i => if i == y then c else k i]; first by rewrite inE. rewrite !ffunE eqxx; congr (_, _); apply/ffunP=> i; rewrite !ffunE. case Eiy: (i == y); last by rewrite Eiy. by rewrite (negbTE nxy) (eqP Eiy). move=> k1 k2 [Eky Epk]; apply/ffunP=> i. have{Epk}: pk k1 i = pk k2 i by rewrite Epk. by rewrite !ffunE; case: eqP => // ->. 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)