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