proposition: Lemma card_n : #|[set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&& (coin2 x == coin3 x)]| = n.
proof: Proof. rewrite -[n]card_ord /coin0 /coin1 /coin2 /coin3. pose f (p : col_squares) := p c3; rewrite -(@card_in_image _ _ f). apply: eq_card => c /=; apply/imageP. exists ([ffun => c] : col_squares); last by rewrite /f ffunE. by rewrite /= inE !ffunE !eqxx. move=> p1 p2; rewrite /= !inE /f -!andbA => eqp1 eqp2 eqp12. apply/eqP; rewrite eqperm_map /= andbT. case/and3P: eqp1; do 3!move/eqP->; case/and3P: eqp2; do 3!move/eqP->. by rewrite !andbb eqp12. 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)