proposition: Lemma card_n2 : forall x y z t : square, uniq [:: x; y; z; t] -> #|[set p : col_squares | (p x == p y) && (p z == p t)]| = (n ^ 2)%N.
proof: Proof. move=> x y z t Uxt; rewrite -[n]card_ord. pose f (p : col_squares) := (p x, p z); rewrite -(@card_in_image _ _ f). rewrite -mulnn -card_prod; apply: eq_card => [] [c d] /=; apply/imageP. rewrite (cat_uniq [::x; y]) in Uxt; case/and3P: Uxt => _. rewrite /= !orbF !andbT => /norP[] /[!inE] nxzt nyzt _. exists [ffun i => if pred2 x y i then c else d]. by rewrite inE !ffunE /= !eqxx orbT (negbTE nxzt) (negbTE nyzt) !eqxx. by rewrite {}/f !ffunE /= eqxx (negbTE nxzt). move=> p1 p2 /[!inE] /andP[p1y p1t] /andP[p2y p2t] [px pz]. have eqp12: all (fun i => p1 i == p2 i) [:: x; y; z; t]. by rewrite /= -(eqP p1y) -(eqP p1t) -(eqP p2y) -(eqP p2t) px pz !eqxx. apply/ffunP=> i; apply/eqP; apply: (allP eqp12). by rewrite (subset_cardP _ (subset_predT _)) // (card_uniqP Uxt) card_ord. 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)