proposition: Lemma tuto_size_tuple : forall (t : n.-tuple T), size t = n.
proof: Proof. move=> f; exact: (eqP (valP f)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)