proposition: Lemma rot_tupleP : forall T n m (t : n.-tuple T), size (rot m t) == n.
proof: Proof. by move=> T n m t; rewrite size_rot size_tuple. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)