proposition: Lemma card_n2_3 : forall 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.
proof: Proof. move=> x y z t u v Uxv; rewrite -[n]card_ord . pose ff (p : col_cubes) := (p x, p t). rewrite -(@card_in_image _ _ ff); first last. move=> p1 p2 /[!inE]; rewrite -!andbA. move=> /and4P[/eqP p1xy /eqP p1yz /eqP p1tu /eqP p1uv]. move=> /and4P[/eqP p2xy/eqP p2yz /eqP p2tu /eqP p2uv] [px pu]. have eqp12: all (fun i => p1 i == p2 i) [:: x; y; z; t; u; v]. by rewrite /= -p1yz -p2yz -p1xy -p2xy -p1uv -p2uv -p1tu -p2tu px pu !eqxx. apply/ffunP=> i; apply/eqP; apply: (allP eqp12). by rewrite (subset_cardP _ (subset_predT _)) // (card_uniqP Uxv) card_ord. rewrite -mulnn -!card_prod; apply: eq_card => [] [c d]/=; apply/imageP. move: Uxv; rewrite (cat_uniq [::x; y; z]) => /= /and3P[Uxt + nuv]. move=> /[!orbF] /norP[] /[!inE] /negPf nxyzt /norP[/negPf nxyzu /negPf nxyzv]. exists [ffun i => if (i \in [:: x; y; z] ) then c else d]. by rewrite /= !(inE, ffunE, eqxx, orbT, nxyzt, nxyzu, nxyzv). by rewrite {}/ff !ffunE !inE /= !eqxx /= nxyzt. 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)