proposition: Lemma tuto_cat_tupleP : forall T n1 n2 (t1 : n1.-tuple T) (t2 : n2.-tuple T), size (t1 ++ t2) == n1 + n2.
proof: Proof. by move=> T n1 n2 t1 t2; rewrite size_cat !size_tuple. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)