proposition: Lemma card_tuple : #|{:n.-tuple T}| = #|T| ^ n.
proof: Proof. by rewrite [#|_|]cardT enumT unlock FinTuple.size_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)