proposition: Lemma eqperm_map : forall p1 p2 : col_squares, (p1 == p2) = all (fun s => p1 s == p2 s) [:: c0; c1; c2; c3].
proof: Proof. move=> p1 p2; apply/eqP/allP=> [-> // | Ep12]; apply/ffunP=> x. by apply/eqP; apply Ep12; case: x; do 4!case=> //. 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)