proposition: Lemma card : #|{: T}| = \sum_i p_ i.
proof: Proof. rewrite card_tagged sumnE/= big_map big_enum. by apply: eq_bigr => i _; rewrite card_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)