proposition: Lemma prod_t_correct : forall (x y : {perm cube}) (i : cube), (x * y) i = nth F0 (prod_tuple (sop x) (sop y)) i.
proof: Proof. move=> x y i; rewrite permM -!sop_spec [RHS](nth_map F0) // size_tuple /=. by rewrite card_ord ltn_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)