fact: Structure tuto_tuple_of : Type := TutoTuple {tuto_tval :> seq T; _ : size tuto_tval == n}.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)