proposition: Lemma card_n3_3 : forall 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.
proof: Proof. move=> x y z t Uxt; rewrite -[n]card_ord. case: (uniq4_uniq6 Uxt) => u [v Uxv]. pose ff (p : col_cubes) := (p x, p u, p v); rewrite -(@card_in_image _ _ ff); first last. move=> p1 p2 /[!inE]; rewrite -!andbA. move=> /and3P[/eqP p1xy /eqP p1yz /eqP p1zt]. move=> /and3P[/eqP p2xy /eqP p2yz /eqP p2zt] [px pu] pv. have eqp12: all (fun i => p1 i == p2 i) [:: x; y; z; t; u; v]. by rewrite /= -p1zt -p2zt -p1yz -p2yz -p1xy -p2xy px pu pv !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[_ hasxt]. rewrite /uniq !inE !andbT => /negPf nuv. exists [ffun i => if i \in [:: x; y; z; t] then c else if u == i then d else e]. by rewrite /= !(inE, ffunE, eqxx, orbT). rewrite {}/ff !(ffunE, inE, eqxx) /=; move: hasxt; rewrite nuv. by do 8![case E: ( _ == _ ); rewrite ?(eqP E)/= ?inE ?eqxx //= ?E {E}]. 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)