proposition: Lemma card_n4 : forall 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.
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 z, p u, p v). rewrite -(@card_in_image _ _ ff); first last. move=> p1 p2 /[!inE] /andP[p1y p1t] /andP[p2y p2t] [px pz] pu pv. have eqp12 : all (fun i => p1 i == p2 i) [:: x; y; z; t; u; v]. by rewrite /= -(eqP p1y) -(eqP p1t) -(eqP p2y) -(eqP p2t) px pz 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 ^ 4 = n * n * n * n)%N by move=> ?; rewrite -!mulnA. rewrite -!card_prod; apply: eq_card => [] [[[c d] e] g] /=; apply/imageP => /=. move: Uxv; rewrite (cat_uniq [:: x; y; z; t]) => /and3P[_]/=; rewrite orbF. move=> /norP[] /[!inE] + + /andP[/negPf nuv _]. rewrite orbA => /norP[/negPf nxyu /negPf nztu]. rewrite orbA => /norP[/negPf nxyv /negPf nztv]. move: Uxt; rewrite (cat_uniq [::x; y]) => /and3P[_]/= /[!(andbT, orbF)]. move=> /norP[] /[!inE] /negPf nxyz /negPf nxyt _. exists [ffun i => if pred2 x y i then c else if pred2 z t i then d else if u == i then e else g]. by rewrite !(inE, ffunE, eqxx,orbT)//= nxyz nxyt. by rewrite {}/ff !ffunE /= !eqxx /= nxyz nxyu nztu nxyv nztv nuv. 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)