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