proposition: Lemma eqperm : forall p1 p2 : {perm cube}, (p1 == p2) = all (fun s => p1 s == p2 s) ecubes.
proof: Proof. move=> p1 p2; apply/eqP/allP=> [-> // | Ep12]; apply/permP=> x. by apply/eqP; rewrite Ep12 // ecubes_def mem_enum. 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)