proposition: Lemma card_bseq n (T : finType) : #|{bseq n of T}| = \sum_(i < n.+1) #|T| ^ i.
proof: Proof. rewrite (bij_eq_card bseq_tagged_tuple_bij) card_tagged sumnE big_map big_enum. by under eq_bigr do rewrite card_tuple. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)