proposition: Lemma card_n3s : forall 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.
proof: Proof. move=> x y z t u v Uxv; rewrite -[n]card_ord . pose ff (p : col_cubes) := (p x, p z, p u). rewrite -(@card_in_image _ _ ff); first last. move=> p1 p2 /[!inE]; rewrite -!andbA. move=> /and3P[/eqP p1xy /eqP p1zt /eqP p1uv]. move=> /and3P[/eqP p2xy /eqP p2zt /eqP p2uv] [px pz] pu. have eqp12: all (fun i => p1 i == p2 i) [:: x; y; z; t; u; v]. by rewrite /= -p1xy -p2xy -p1zt -p2zt -p1uv -p2uv px pz pu !eqxx. apply/ffunP=> i; apply/eqP; apply: (allP eqp12). by rewrite (subset_cardP _ (subset_predT _)) // (card_uniqP Uxv) card_ord. have -> : forall n, (n ^ 3 = n * n * n)%N by move=> ?; rewrite -!mulnA. rewrite -!card_prod; apply: eq_card => [] [[c d] e] /=; apply/imageP. move: Uxv; rewrite (cat_uniq [::x; y; z; t]) => /and3P[Uxt + nuv]. move=> /= /[!orbF] /norP[] /[!inE]. rewrite orbA => /norP[/negPf nxyu /negPf nztu]. rewrite orbA => /norP[/negPf nxyv /negPf nztv]. move: Uxt; rewrite (cat_uniq [::x; y]) => /and3P[_]. rewrite /= !orbF !andbT => /norP[] /[!inE] /negPf nxyz /negPf nxyt _. exists [ffun i => if i \in [:: x; y] then c else if i \in [:: z; t] then d else e]. by rewrite !(inE, ffunE, eqxx,orbT)//= nxyz nxyt nxyu nztu nxyv nztv !eqxx. by rewrite {}/ff !ffunE !inE /= !eqxx nxyz nxyu nztu. 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)